Theorem ancomsd 269

Description: Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)

Hypothesis

Ref	Expression
ancomsd.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
ancomsd	⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

Proof of Theorem ancomsd

Step	Hyp	Ref	Expression
1		ancom 266	. 2 ⊢ ((𝜒 ∧ 𝜓) ↔ (𝜓 ∧ 𝜒))
2		ancomsd.1	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	1, 2	biimtrid 152	1 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylan2d  294  mpand  433  anabsi6  586  ralxfrd  4610  rexxfrd  4611  poirr2  5183  smoel  6575  genprndl  7895  genprndu  7896  addcanprlemu  7989  leltadd  8783  lemul12b  9200  lbzbi  10033  dvdssub2  12628  odzdvds  13054  wlk1walkdom  16817