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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  elres  4811  relbrcnvg  4874  fvelrnb  5421  relelec  6420  prcdnql  7233  1idpru  7340  gt0srpr  7484  focdmex  10419  fihashf1rn  10421  sinbnd  11303  cosbnd  11304  dvdsdivcl  11389  nn0ehalf  11441  nn0oddm1d2  11447  nnoddm1d2  11448  coprmgcdb  11608  divgcdcoprm0  11621  divgcdcoprmex  11622  cncongr1  11623