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  5017  relbrcnvg  5083  fvelrnb  5654  relelec  6692  prcdnql  7639  1idpru  7746  gt0srpr  7903  fihashf1rn  10977  pfxccatin12  11231  prodmodclem3  12052  sinbnd  12229  cosbnd  12230  dvdsdivcl  12327  nn0ehalf  12380  nn0oddm1d2  12386  nnoddm1d2  12387  coprmgcdb  12576  divgcdcoprm0  12589  divgcdcoprmex  12590  cncongr1  12591  quscrng  14462  sincosq2sgn  15466  sincosq4sgn  15468