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  5040  relbrcnvg  5106  fvelrnb  5680  relelec  6720  prcdnql  7667  1idpru  7774  gt0srpr  7931  fihashf1rn  11005  pfxccatin12  11260  prodmodclem3  12081  sinbnd  12258  cosbnd  12259  dvdsdivcl  12356  nn0ehalf  12409  nn0oddm1d2  12415  nnoddm1d2  12416  coprmgcdb  12605  divgcdcoprm0  12618  divgcdcoprmex  12619  cncongr1  12620  quscrng  14491  sincosq2sgn  15495  sincosq4sgn  15497