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

Step	Hyp	Ref	Expression
1		ancomd.1	. 2 |- ( ph -> ( ps /\ ch ) )
2		ancom 263	. 2 |- ( ( ps /\ ch ) <-> ( ch /\ ps ) )
3	1, 2	sylib 121	1 |- ( ph -> ( ch /\ ps ) )

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