Theorem ancomd 265

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 264	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
3	1, 2	sylib 121	1 ⊢ (𝜑 → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  elres  4855  relbrcnvg  4918  fvelrnb  5469  relelec  6469  prcdnql  7292  1idpru  7399  gt0srpr  7556  focdmex  10533  fihashf1rn  10535  prodmodclem3  11344  sinbnd  11459  cosbnd  11460  dvdsdivcl  11548  nn0ehalf  11600  nn0oddm1d2  11606  nnoddm1d2  11607  coprmgcdb  11769  divgcdcoprm0  11782  divgcdcoprmex  11783  cncongr1  11784  sincosq2sgn  12908  sincosq4sgn  12910