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

Theorem ancomd 265
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 264 . 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-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  4855  relbrcnvg  4918  fvelrnb  5469  relelec  6469  prcdnql  7299  1idpru  7406  gt0srpr  7563  focdmex  10540  fihashf1rn  10542  prodmodclem3  11351  sinbnd  11466  cosbnd  11467  dvdsdivcl  11555  nn0ehalf  11607  nn0oddm1d2  11613  nnoddm1d2  11614  coprmgcdb  11776  divgcdcoprm0  11789  divgcdcoprmex  11790  cncongr1  11791  sincosq2sgn  12921  sincosq4sgn  12923
  Copyright terms: Public domain W3C validator