Theorem sylan2d 617

Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)

Hypotheses

Ref	Expression
sylan2d.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylan2d.2	⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜏))

Assertion

Ref	Expression
sylan2d	⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜏))

Proof of Theorem sylan2d

Step	Hyp	Ref	Expression
1		sylan2d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylan2d.2	. . . 4 ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜏))
3	2	ancomsd 471	. . 3 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏))
4	1, 3	syland 615	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏))
5	4	ancomsd 471	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜏))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylan2i  618  syl2and  620  swopo  5570  fprlem1  8302  unblem1  9268  frrlem15  9745  prodgt02  12146  lo1mul  15775  infpnlem1  17068  matunitlindflem1  22974  ghmcnp  24414  ulmcaulem  26703  ulmcau  26704  shintcli  31913  ballotlemfc0  35108  ballotlemfcc  35109  kardfi  35811  btwnxfr  36791  endofsegid  36820  bj-bary1lem1  38200  ltcvrntr  40449  poml4N  40978