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  4979  relbrcnvg  5045  fvelrnb  5605  relelec  6631  prcdnql  7546  1idpru  7653  gt0srpr  7810  fihashf1rn  10862  prodmodclem3  11721  sinbnd  11898  cosbnd  11899  dvdsdivcl  11995  nn0ehalf  12047  nn0oddm1d2  12053  nnoddm1d2  12054  coprmgcdb  12229  divgcdcoprm0  12242  divgcdcoprmex  12243  cncongr1  12244  quscrng  14032  sincosq2sgn  15003  sincosq4sgn  15005