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  5074  relbrcnvg  5141  fvelrnb  5724  relelec  6809  prcdnql  7799  1idpru  7906  gt0srpr  8063  fihashf1rn  11151  pfxccatin12  11425  prodmodclem3  12261  sinbnd  12438  cosbnd  12439  dvdsdivcl  12536  nn0ehalf  12589  nn0oddm1d2  12595  nnoddm1d2  12596  coprmgcdb  12785  divgcdcoprm0  12798  divgcdcoprmex  12799  cncongr1  12800  quscrng  14681  sincosq2sgn  15692  sincosq4sgn  15694  subupgr  16268