Theorem sylan2d 603

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  sylan2i  604  syl2and  606  swopo  5598  fprlem1  8287  wfrlem5OLD  8315  unblem1  9297  unfiOLD  9315  frrlem15  9754  prodgt02  12066  lo1mul  15576  infpnlem1  16847  ghmcnp  23839  ulmcaulem  26142  ulmcau  26143  shintcli  30849  ballotlemfc0  33789  ballotlemfcc  33790  btwnxfr  35332  endofsegid  35361  bj-bary1lem1  36495  matunitlindflem1  36787  ltcvrntr  38598  poml4N  39127