Nearby theorems
|
|
bfol.mm Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > PE Home > Th. List > wff-rcp-AND5 | |||
| Description: Extend WFF definition to include '∧' 5-Tuple. |
| Ref | Expression |
|---|---|
| wff-ph1 | wff 𝜑₁ |
| wff-ph2 | wff 𝜑₂ |
| wff-ph3 | wff 𝜑₃ |
| wff-ph4 | wff 𝜑₄ |
| wff-ph5 | wff 𝜑₅ |
| Ref | Expression |
|---|---|
| wff-rcp-AND5 | wff (𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄ ∧ 𝜑₅) |
| Colors of variables: wff objvar term class |
| Copyright terms: Public domain | W3C validator |