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  5000  relbrcnvg  5066  fvelrnb  5633  relelec  6669  prcdnql  7604  1idpru  7711  gt0srpr  7868  fihashf1rn  10940  prodmodclem3  11930  sinbnd  12107  cosbnd  12108  dvdsdivcl  12205  nn0ehalf  12258  nn0oddm1d2  12264  nnoddm1d2  12265  coprmgcdb  12454  divgcdcoprm0  12467  divgcdcoprmex  12468  cncongr1  12469  quscrng  14339  sincosq2sgn  15343  sincosq4sgn  15345