![]() |
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 282 | 1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: an42s 559 ordsuc 4416 xpexr2m 4916 f1elima 5606 f1imaeq 5608 isosolem 5657 caovlem2d 5895 2ndconst 6049 isotilem 6808 prarloclem4 7207 mulsub 8030 leltadd 8076 eqord1 8112 divmul24ap 8337 blcomps 12324 blcom 12325 |
Copyright terms: Public domain | W3C validator |