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  5041  relbrcnvg  5107  fvelrnb  5683  relelec  6730  prcdnql  7679  1idpru  7786  gt0srpr  7943  fihashf1rn  11018  pfxccatin12  11273  prodmodclem3  12094  sinbnd  12271  cosbnd  12272  dvdsdivcl  12369  nn0ehalf  12422  nn0oddm1d2  12428  nnoddm1d2  12429  coprmgcdb  12618  divgcdcoprm0  12631  divgcdcoprmex  12632  cncongr1  12633  quscrng  14505  sincosq2sgn  15509  sincosq4sgn  15511