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  4992  relbrcnvg  5058  fvelrnb  5620  relelec  6652  prcdnql  7579  1idpru  7686  gt0srpr  7843  fihashf1rn  10914  prodmodclem3  11805  sinbnd  11982  cosbnd  11983  dvdsdivcl  12080  nn0ehalf  12133  nn0oddm1d2  12139  nnoddm1d2  12140  coprmgcdb  12329  divgcdcoprm0  12342  divgcdcoprmex  12343  cncongr1  12344  quscrng  14213  sincosq2sgn  15217  sincosq4sgn  15219