Theorem sylan2d 500

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 469	. . 3 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏))
4	1, 3	syland 499	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏))
5	4	ancomsd 469	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜏))

Syntax hints:   → wi 4   ∧ wa 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 385

This theorem is referenced by:  syl2and  501  sylan2i  690  swopo  5197  wfrlem5  7589  unblem1  8379  unfi  8394  prodgt02  11081  prodge02  11083  lo1mul  14577  infpnlem1  15836  ghmcnp  22139  ulmcaulem  24367  ulmcau  24368  shintcli  28518  ballotlemfc0  30884  ballotlemfcc  30885  frrlem5  32111  btwnxfr  32490  endofsegid  32519  bj-bary1lem1  33490  matunitlindflem1  33736  ltcvrntr  35231  poml4N  35760