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  5041  relbrcnvg  5107  fvelrnb  5681  relelec  6722  prcdnql  7671  1idpru  7778  gt0srpr  7935  fihashf1rn  11010  pfxccatin12  11265  prodmodclem3  12086  sinbnd  12263  cosbnd  12264  dvdsdivcl  12361  nn0ehalf  12414  nn0oddm1d2  12420  nnoddm1d2  12421  coprmgcdb  12610  divgcdcoprm0  12623  divgcdcoprmex  12624  cncongr1  12625  quscrng  14497  sincosq2sgn  15501  sincosq4sgn  15503