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  5047  relbrcnvg  5113  fvelrnb  5689  relelec  6739  prcdnql  7697  1idpru  7804  gt0srpr  7961  fihashf1rn  11043  pfxccatin12  11307  prodmodclem3  12129  sinbnd  12306  cosbnd  12307  dvdsdivcl  12404  nn0ehalf  12457  nn0oddm1d2  12463  nnoddm1d2  12464  coprmgcdb  12653  divgcdcoprm0  12666  divgcdcoprmex  12667  cncongr1  12668  quscrng  14540  sincosq2sgn  15544  sincosq4sgn  15546