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  5051  relbrcnvg  5117  fvelrnb  5696  relelec  6749  prcdnql  7709  1idpru  7816  gt0srpr  7973  fihashf1rn  11056  pfxccatin12  11323  prodmodclem3  12159  sinbnd  12336  cosbnd  12337  dvdsdivcl  12434  nn0ehalf  12487  nn0oddm1d2  12493  nnoddm1d2  12494  coprmgcdb  12683  divgcdcoprm0  12696  divgcdcoprmex  12697  cncongr1  12698  quscrng  14571  sincosq2sgn  15580  sincosq4sgn  15582  subupgr  16153