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  5079  relbrcnvg  5146  fvelrnb  5729  relelec  6822  prcdnql  7815  1idpru  7922  gt0srpr  8079  fihashf1rn  11179  pfxccatin12  11453  prodmodclem3  12289  sinbnd  12466  cosbnd  12467  dvdsdivcl  12564  nn0ehalf  12617  nn0oddm1d2  12623  nnoddm1d2  12624  coprmgcdb  12813  divgcdcoprm0  12826  divgcdcoprmex  12827  cncongr1  12828  quscrng  14810  sincosq2sgn  15821  sincosq4sgn  15823  subupgr  16397