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  5073  relbrcnvg  5140  fvelrnb  5723  relelec  6808  prcdnql  7795  1idpru  7902  gt0srpr  8059  fihashf1rn  11146  pfxccatin12  11418  prodmodclem3  12254  sinbnd  12431  cosbnd  12432  dvdsdivcl  12529  nn0ehalf  12582  nn0oddm1d2  12588  nnoddm1d2  12589  coprmgcdb  12778  divgcdcoprm0  12791  divgcdcoprmex  12792  cncongr1  12793  quscrng  14668  sincosq2sgn  15679  sincosq4sgn  15681  subupgr  16255