Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ancomd | GIF version |
Description: Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.) |
Ref | Expression |
---|---|
ancomd.1 | ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
Ref | Expression |
---|---|
ancomd | ⊢ (𝜑 → (𝜒 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancomd.1 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) | |
2 | ancom 264 | . 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) | |
3 | 1, 2 | sylib 121 | 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 depends on definitions: df-bi 116 |
This theorem is referenced by: elres 4850 relbrcnvg 4913 fvelrnb 5462 relelec 6462 prcdnql 7285 1idpru 7392 gt0srpr 7549 focdmex 10526 fihashf1rn 10528 sinbnd 11448 cosbnd 11449 dvdsdivcl 11537 nn0ehalf 11589 nn0oddm1d2 11595 nnoddm1d2 11596 coprmgcdb 11758 divgcdcoprm0 11771 divgcdcoprmex 11772 cncongr1 11773 sincosq2sgn 12897 sincosq4sgn 12899 |
Copyright terms: Public domain | W3C validator |