Theorem ancomd 267

Description: Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.)

Hypothesis

Ref	Expression
ancomd.1	⊢ (𝜑 → (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
ancomd	⊢ (𝜑 → (𝜒 ∧ 𝜓))

Proof of Theorem ancomd

Step	Hyp	Ref	Expression
1		ancomd.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
2		ancom 266	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
3	1, 2	sylib 122	1 ⊢ (𝜑 → (𝜒 ∧ 𝜓))

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  4983  relbrcnvg  5049  fvelrnb  5611  relelec  6643  prcdnql  7570  1idpru  7677  gt0srpr  7834  fihashf1rn  10899  prodmodclem3  11759  sinbnd  11936  cosbnd  11937  dvdsdivcl  12034  nn0ehalf  12087  nn0oddm1d2  12093  nnoddm1d2  12094  coprmgcdb  12283  divgcdcoprm0  12296  divgcdcoprmex  12297  cncongr1  12298  quscrng  14167  sincosq2sgn  15149  sincosq4sgn  15151