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  4925  relbrcnvg  4988  fvelrnb  5542  relelec  6550  prcdnql  7435  1idpru  7542  gt0srpr  7699  focdmex  10710  fihashf1rn  10712  prodmodclem3  11527  sinbnd  11704  cosbnd  11705  dvdsdivcl  11799  nn0ehalf  11851  nn0oddm1d2  11857  nnoddm1d2  11858  coprmgcdb  12031  divgcdcoprm0  12044  divgcdcoprmex  12045  cncongr1  12046  sincosq2sgn  13503  sincosq4sgn  13505