Theorem sylan2d 605

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  sylan2i  606  syl2and  608  swopo  5543  fprlem1  8242  unblem1  9192  frrlem15  9669  prodgt02  11989  lo1mul  15551  infpnlem1  16838  ghmcnp  24059  ulmcaulem  26359  ulmcau  26360  shintcli  31404  ballotlemfc0  34650  ballotlemfcc  34651  btwnxfr  36250  endofsegid  36279  bj-bary1lem1  37512  matunitlindflem1  37813  ltcvrntr  39680  poml4N  40209