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  6853  prcdnql  7857  1idpru  7964  gt0srpr  8121  fihashf1rn  11249  pfxccatin12  11527  prodmodclem3  12367  sinbnd  12544  cosbnd  12545  dvdsdivcl  12642  nn0ehalf  12695  nn0oddm1d2  12701  nnoddm1d2  12702  coprmgcdb  12891  divgcdcoprm0  12904  divgcdcoprmex  12905  cncongr1  12906  quscrng  14979  sincosq2sgn  16054  sincosq4sgn  16056  subupgr  16719