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  4920  relbrcnvg  4983  fvelrnb  5534  relelec  6541  prcdnql  7425  1idpru  7532  gt0srpr  7689  focdmex  10700  fihashf1rn  10702  prodmodclem3  11516  sinbnd  11693  cosbnd  11694  dvdsdivcl  11788  nn0ehalf  11840  nn0oddm1d2  11846  nnoddm1d2  11847  coprmgcdb  12020  divgcdcoprm0  12033  divgcdcoprmex  12034  cncongr1  12035  sincosq2sgn  13388  sincosq4sgn  13390