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  4978  relbrcnvg  5044  fvelrnb  5604  relelec  6629  prcdnql  7544  1idpru  7651  gt0srpr  7808  fihashf1rn  10859  prodmodclem3  11718  sinbnd  11895  cosbnd  11896  dvdsdivcl  11992  nn0ehalf  12044  nn0oddm1d2  12050  nnoddm1d2  12051  coprmgcdb  12226  divgcdcoprm0  12239  divgcdcoprmex  12240  cncongr1  12241  quscrng  14029  sincosq2sgn  14962  sincosq4sgn  14964