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  5076  relbrcnvg  5143  fvelrnb  5726  relelec  6811  prcdnql  7804  1idpru  7911  gt0srpr  8068  fihashf1rn  11159  pfxccatin12  11433  prodmodclem3  12269  sinbnd  12446  cosbnd  12447  dvdsdivcl  12544  nn0ehalf  12597  nn0oddm1d2  12603  nnoddm1d2  12604  coprmgcdb  12793  divgcdcoprm0  12806  divgcdcoprmex  12807  cncongr1  12808  quscrng  14730  sincosq2sgn  15741  sincosq4sgn  15743  subupgr  16317