Theorem ancomd 263

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  elres  4668  relbrcnvg  4728  fvelrnb  5247  relelec  6205  prcdnql  6725  1idpru  6832  gt0srpr  6976  focdmex  9800  sizef1rn  9802  dvdsdivcl  10384  nn0ehalf  10436  nn0oddm1d2  10442  nnoddm1d2  10443  coprmgcdb  10603  divgcdcoprm0  10616  divgcdcoprmex  10617  cncongr1  10618