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  5094  relbrcnvg  5161  fvelrnb  5744  relelec  6839  prcdnql  7841  1idpru  7948  gt0srpr  8105  fihashf1rn  11205  pfxccatin12  11483  prodmodclem3  12320  sinbnd  12497  cosbnd  12498  dvdsdivcl  12595  nn0ehalf  12648  nn0oddm1d2  12654  nnoddm1d2  12655  coprmgcdb  12844  divgcdcoprm0  12857  divgcdcoprmex  12858  cncongr1  12859  quscrng  14842  sincosq2sgn  15851  sincosq4sgn  15853  subupgr  16428