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  4994  relbrcnvg  5060  fvelrnb  5625  relelec  6661  prcdnql  7596  1idpru  7703  gt0srpr  7860  fihashf1rn  10931  prodmodclem3  11857  sinbnd  12034  cosbnd  12035  dvdsdivcl  12132  nn0ehalf  12185  nn0oddm1d2  12191  nnoddm1d2  12192  coprmgcdb  12381  divgcdcoprm0  12394  divgcdcoprmex  12395  cncongr1  12396  quscrng  14266  sincosq2sgn  15270  sincosq4sgn  15272