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  5004  relbrcnvg  5070  fvelrnb  5639  relelec  6675  prcdnql  7617  1idpru  7724  gt0srpr  7881  fihashf1rn  10955  prodmodclem3  11961  sinbnd  12138  cosbnd  12139  dvdsdivcl  12236  nn0ehalf  12289  nn0oddm1d2  12295  nnoddm1d2  12296  coprmgcdb  12485  divgcdcoprm0  12498  divgcdcoprmex  12499  cncongr1  12500  quscrng  14370  sincosq2sgn  15374  sincosq4sgn  15376