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  5079  relbrcnvg  5146  fvelrnb  5729  relelec  6822  prcdnql  7815  1idpru  7922  gt0srpr  8079  fihashf1rn  11176  pfxccatin12  11450  prodmodclem3  12286  sinbnd  12463  cosbnd  12464  dvdsdivcl  12561  nn0ehalf  12614  nn0oddm1d2  12620  nnoddm1d2  12621  coprmgcdb  12810  divgcdcoprm0  12823  divgcdcoprmex  12824  cncongr1  12825  quscrng  14807  sincosq2sgn  15818  sincosq4sgn  15820  subupgr  16394