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  4982  relbrcnvg  5048  fvelrnb  5608  relelec  6634  prcdnql  7551  1idpru  7658  gt0srpr  7815  fihashf1rn  10880  prodmodclem3  11740  sinbnd  11917  cosbnd  11918  dvdsdivcl  12015  nn0ehalf  12068  nn0oddm1d2  12074  nnoddm1d2  12075  coprmgcdb  12256  divgcdcoprm0  12269  divgcdcoprmex  12270  cncongr1  12271  quscrng  14089  sincosq2sgn  15063  sincosq4sgn  15065