Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ancomd GIF version

Theorem ancomd 263
 Description: Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.)
Hypothesis
Ref Expression
ancomd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ancomd (𝜑 → (𝜒𝜓))

Proof of Theorem ancomd
StepHypRef Expression
1 ancomd.1 . 2 (𝜑 → (𝜓𝜒))
2 ancom 262 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 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