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

Step	Hyp	Ref	Expression
1		ancomd.1	. 2 |- ( ph -> ( ps /\ ch ) )
2		ancom 264	. 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-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  4863  relbrcnvg  4926  fvelrnb  5477  relelec  6477  prcdnql  7316  1idpru  7423  gt0srpr  7580  focdmex  10565  fihashf1rn  10567  prodmodclem3  11376  sinbnd  11495  cosbnd  11496  dvdsdivcl  11584  nn0ehalf  11636  nn0oddm1d2  11642  nnoddm1d2  11643  coprmgcdb  11805  divgcdcoprm0  11818  divgcdcoprmex  11819  cncongr1  11820  sincosq2sgn  12956  sincosq4sgn  12958