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  5044  relbrcnvg  5110  fvelrnb  5686  relelec  6735  prcdnql  7687  1idpru  7794  gt0srpr  7951  fihashf1rn  11027  pfxccatin12  11286  prodmodclem3  12107  sinbnd  12284  cosbnd  12285  dvdsdivcl  12382  nn0ehalf  12435  nn0oddm1d2  12441  nnoddm1d2  12442  coprmgcdb  12631  divgcdcoprm0  12644  divgcdcoprmex  12645  cncongr1  12646  quscrng  14518  sincosq2sgn  15522  sincosq4sgn  15524