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  5575  fprlem1  8349  unblem1  9315  frrlem15  9791  prodgt02  12195  lo1mul  15827  infpnlem1  17120  matunitlindflem1  23027  ghmcnp  24467  ulmcaulem  26754  ulmcau  26755  shintcli  31964  ballotlemfc0  35208  ballotlemfcc  35209  kardfi  35951  btwnxfr  37012  endofsegid  37041  bj-bary1lem1  38437  ltcvrntr  40684  poml4N  41213