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

Theorem ancomd 264
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 263 . 2  |-  ( ( ps  /\  ch )  <->  ( ch  /\  ps )
)
31, 2sylib 121 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  elres  4763  relbrcnvg  4826  fvelrnb  5367  relelec  6348  prcdnql  7106  1idpru  7213  gt0srpr  7357  focdmex  10258  fihashf1rn  10260  sinbnd  11106  cosbnd  11107  dvdsdivcl  11192  nn0ehalf  11244  nn0oddm1d2  11250  nnoddm1d2  11251  coprmgcdb  11411  divgcdcoprm0  11424  divgcdcoprmex  11425  cncongr1  11426
  Copyright terms: Public domain W3C validator