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  5015  relbrcnvg  5081  fvelrnb  5651  relelec  6687  prcdnql  7634  1idpru  7741  gt0srpr  7898  fihashf1rn  10972  pfxccatin12  11226  prodmodclem3  12047  sinbnd  12224  cosbnd  12225  dvdsdivcl  12322  nn0ehalf  12375  nn0oddm1d2  12381  nnoddm1d2  12382  coprmgcdb  12571  divgcdcoprm0  12584  divgcdcoprmex  12585  cncongr1  12586  quscrng  14456  sincosq2sgn  15460  sincosq4sgn  15462