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 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))

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:  sylan2d  294  mpand  429  anabsi6  580  ralxfrd  4557  rexxfrd  4558  poirr2  5127  smoel  6461  genprndl  7734  genprndu  7735  addcanprlemu  7828  leltadd  8620  lemul12b  9034  lbzbi  9843  dvdssub2  12389  odzdvds  12811  wlk1walkdom  16170