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  5101  relbrcnvg  5169  fvelrnb  5753  relelec  6853  prcdnql  7858  1idpru  7965  gt0srpr  8122  fihashf1rn  11250  pfxccatin12  11528  prodmodclem3  12368  sinbnd  12545  cosbnd  12546  dvdsdivcl  12643  nn0ehalf  12696  nn0oddm1d2  12702  nnoddm1d2  12703  coprmgcdb  12892  divgcdcoprm0  12905  divgcdcoprmex  12906  cncongr1  12907  quscrng  14980  sincosq2sgn  16066  sincosq4sgn  16068  subupgr  16731