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

Theorem ancomd 267
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 266 . 2  |-  ( ( ps  /\  ch )  <->  ( ch  /\  ps )
)
31, 2sylib 122 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  elres  4964  relbrcnvg  5028  fvelrnb  5587  relelec  6605  prcdnql  7518  1idpru  7625  gt0srpr  7782  fihashf1rn  10809  prodmodclem3  11624  sinbnd  11801  cosbnd  11802  dvdsdivcl  11897  nn0ehalf  11949  nn0oddm1d2  11955  nnoddm1d2  11956  coprmgcdb  12131  divgcdcoprm0  12144  divgcdcoprmex  12145  cncongr1  12146  quscrng  13872  sincosq2sgn  14733  sincosq4sgn  14735
  Copyright terms: Public domain W3C validator