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

Theorem ancomd 265
 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 264 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 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  4863  relbrcnvg  4926  fvelrnb  5477  relelec  6477  prcdnql  7317  1idpru  7424  gt0srpr  7581  focdmex  10566  fihashf1rn  10568  prodmodclem3  11377  sinbnd  11496  cosbnd  11497  dvdsdivcl  11585  nn0ehalf  11637  nn0oddm1d2  11643  nnoddm1d2  11644  coprmgcdb  11806  divgcdcoprm0  11819  divgcdcoprmex  11820  cncongr1  11821  sincosq2sgn  12957  sincosq4sgn  12959
 Copyright terms: Public domain W3C validator