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 4914 relbrcnvg 4977 fvelrnb 5528 relelec 6532 prcdnql 7416 1idpru 7523 gt0srpr 7680 focdmex 10689 fihashf1rn 10691 prodmodclem3 11502 sinbnd 11679 cosbnd 11680 dvdsdivcl 11773 nn0ehalf 11825 nn0oddm1d2 11831 nnoddm1d2 11832 coprmgcdb 11999 divgcdcoprm0 12012 divgcdcoprmex 12013 cncongr1 12014 sincosq2sgn 13295 sincosq4sgn 13297 |
Copyright terms: Public domain | W3C validator |