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  4927  relbrcnvg  4990  fvelrnb  5544  relelec  6553  prcdnql  7446  1idpru  7553  gt0srpr  7710  focdmex  10721  fihashf1rn  10723  prodmodclem3  11538  sinbnd  11715  cosbnd  11716  dvdsdivcl  11810  nn0ehalf  11862  nn0oddm1d2  11868  nnoddm1d2  11869  coprmgcdb  12042  divgcdcoprm0  12055  divgcdcoprmex  12056  cncongr1  12057  sincosq2sgn  13542  sincosq4sgn  13544