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 4927 relbrcnvg 4990 fvelrnb 5544 relelec 6553 prcdnql 7446 1idpru 7553 gt0srpr 7710 focdmex 10721 fihashf1rn 10723 prodmodclem3 11538 sinbnd 11715 cosbnd 11716 dvdsdivcl 11810 nn0ehalf 11862 nn0oddm1d2 11868 nnoddm1d2 11869 coprmgcdb 12042 divgcdcoprm0 12055 divgcdcoprmex 12056 cncongr1 12057 sincosq2sgn 13542 sincosq4sgn 13544 |
Copyright terms: Public domain | W3C validator |