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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  elres  5101  relbrcnvg  5169  fvelrnb  5753  relelec  6854  prcdnql  7857  1idpru  7964  gt0srpr  8121  fihashf1rn  11248  pfxccatin12  11526  prodmodclem3  12366  sinbnd  12543  cosbnd  12544  dvdsdivcl  12641  nn0ehalf  12694  nn0oddm1d2  12700  nnoddm1d2  12701  coprmgcdb  12890  divgcdcoprm0  12903  divgcdcoprmex  12904  cncongr1  12905  quscrng  14978  sincosq2sgn  16071  sincosq4sgn  16073  subupgr  16736