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 ⊢ (𝜑 → (𝜒 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  elres  5099  relbrcnvg  5166  fvelrnb  5750  relelec  6849  prcdnql  7851  1idpru  7958  gt0srpr  8115  fihashf1rn  11229  pfxccatin12  11507  prodmodclem3  12344  sinbnd  12521  cosbnd  12522  dvdsdivcl  12619  nn0ehalf  12672  nn0oddm1d2  12678  nnoddm1d2  12679  coprmgcdb  12868  divgcdcoprm0  12881  divgcdcoprmex  12882  cncongr1  12883  quscrng  14872  sincosq2sgn  15931  sincosq4sgn  15933  subupgr  16526