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  5049  relbrcnvg  5115  fvelrnb  5693  relelec  6744  prcdnql  7704  1idpru  7811  gt0srpr  7968  fihashf1rn  11051  pfxccatin12  11315  prodmodclem3  12138  sinbnd  12315  cosbnd  12316  dvdsdivcl  12413  nn0ehalf  12466  nn0oddm1d2  12472  nnoddm1d2  12473  coprmgcdb  12662  divgcdcoprm0  12675  divgcdcoprmex  12676  cncongr1  12677  quscrng  14550  sincosq2sgn  15554  sincosq4sgn  15556  subupgr  16127