![]() |
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 262 | . 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) | |
3 | 1, 2 | sylib 120 | 1 ⊢ (𝜑 → (𝜒 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: elres 4668 relbrcnvg 4728 fvelrnb 5247 relelec 6205 prcdnql 6725 1idpru 6832 gt0srpr 6976 focdmex 9800 sizef1rn 9802 dvdsdivcl 10384 nn0ehalf 10436 nn0oddm1d2 10442 nnoddm1d2 10443 coprmgcdb 10603 divgcdcoprm0 10616 divgcdcoprmex 10617 cncongr1 10618 |
Copyright terms: Public domain | W3C validator |