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  5055  relbrcnvg  5122  fvelrnb  5702  relelec  6787  prcdnql  7747  1idpru  7854  gt0srpr  8011  fihashf1rn  11096  pfxccatin12  11363  prodmodclem3  12199  sinbnd  12376  cosbnd  12377  dvdsdivcl  12474  nn0ehalf  12527  nn0oddm1d2  12533  nnoddm1d2  12534  coprmgcdb  12723  divgcdcoprm0  12736  divgcdcoprmex  12737  cncongr1  12738  quscrng  14612  sincosq2sgn  15621  sincosq4sgn  15623  subupgr  16197