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

Theorem ancomd 263
Description: Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.)
Hypothesis
Ref Expression
ancomd.1  |-  ( ph  ->  ( ps  /\  ch ) )
Assertion
Ref Expression
ancomd  |-  ( ph  ->  ( ch  /\  ps ) )

Proof of Theorem ancomd
StepHypRef Expression
1 ancomd.1 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
2 ancom 262 . 2  |-  ( ( ps  /\  ch )  <->  ( ch  /\  ps )
)
31, 2sylib 120 1  |-  ( ph  ->  ( ch  /\  ps ) )
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