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  5099  relbrcnvg  5166  fvelrnb  5750  relelec  6849  prcdnql  7852  1idpru  7959  gt0srpr  8116  fihashf1rn  11243  pfxccatin12  11521  prodmodclem3  12361  sinbnd  12538  cosbnd  12539  dvdsdivcl  12636  nn0ehalf  12689  nn0oddm1d2  12695  nnoddm1d2  12696  coprmgcdb  12885  divgcdcoprm0  12898  divgcdcoprmex  12899  cncongr1  12900  quscrng  14954  sincosq2sgn  16020  sincosq4sgn  16022  subupgr  16680