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  5049  relbrcnvg  5115  fvelrnb  5693  relelec  6743  prcdnql  7703  1idpru  7810  gt0srpr  7967  fihashf1rn  11049  pfxccatin12  11313  prodmodclem3  12135  sinbnd  12312  cosbnd  12313  dvdsdivcl  12410  nn0ehalf  12463  nn0oddm1d2  12469  nnoddm1d2  12470  coprmgcdb  12659  divgcdcoprm0  12672  divgcdcoprmex  12673  cncongr1  12674  quscrng  14546  sincosq2sgn  15550  sincosq4sgn  15552  subupgr  16123