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  5097  relbrcnvg  5164  fvelrnb  5747  relelec  6843  prcdnql  7845  1idpru  7952  gt0srpr  8109  fihashf1rn  11210  pfxccatin12  11488  prodmodclem3  12325  sinbnd  12502  cosbnd  12503  dvdsdivcl  12600  nn0ehalf  12653  nn0oddm1d2  12659  nnoddm1d2  12660  coprmgcdb  12849  divgcdcoprm0  12862  divgcdcoprmex  12863  cncongr1  12864  quscrng  14853  sincosq2sgn  15911  sincosq4sgn  15913  subupgr  16497