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

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

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  4944  relbrcnvg  5008  fvelrnb  5564  relelec  6575  prcdnql  7483  1idpru  7590  gt0srpr  7747  fihashf1rn  10768  prodmodclem3  11583  sinbnd  11760  cosbnd  11761  dvdsdivcl  11856  nn0ehalf  11908  nn0oddm1d2  11914  nnoddm1d2  11915  coprmgcdb  12088  divgcdcoprm0  12101  divgcdcoprmex  12102  cncongr1  12103  sincosq2sgn  14251  sincosq4sgn  14253