Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ancom2s | GIF version |
Description: Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
Ref | Expression |
---|---|
an12s.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Ref | Expression |
---|---|
ancom2s | ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.22 263 | . 2 ⊢ ((𝜒 ∧ 𝜓) → (𝜓 ∧ 𝜒)) | |
2 | an12s.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylan2 284 | 1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: an42s 578 ordsuc 4478 xpexr2m 4980 f1elima 5674 f1imaeq 5676 isosolem 5725 caovlem2d 5963 2ndconst 6119 isotilem 6893 prarloclem4 7306 mulsub 8163 leltadd 8209 eqord1 8245 divmul24ap 8476 blcomps 12565 blcom 12566 |
Copyright terms: Public domain | W3C validator |