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  4850  relbrcnvg  4913  fvelrnb  5462  relelec  6462  prcdnql  7285  1idpru  7392  gt0srpr  7549  focdmex  10526  fihashf1rn  10528  sinbnd  11448  cosbnd  11449  dvdsdivcl  11537  nn0ehalf  11589  nn0oddm1d2  11595  nnoddm1d2  11596  coprmgcdb  11758  divgcdcoprm0  11771  divgcdcoprmex  11772  cncongr1  11773  sincosq2sgn  12897  sincosq4sgn  12899