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  4936  relbrcnvg  5000  fvelrnb  5555  relelec  6565  prcdnql  7458  1idpru  7565  gt0srpr  7722  fihashf1rn  10736  prodmodclem3  11551  sinbnd  11728  cosbnd  11729  dvdsdivcl  11823  nn0ehalf  11875  nn0oddm1d2  11881  nnoddm1d2  11882  coprmgcdb  12055  divgcdcoprm0  12068  divgcdcoprmex  12069  cncongr1  12070  sincosq2sgn  13819  sincosq4sgn  13821