Theorem syland 606

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

Hypotheses

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

Assertion

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

Proof of Theorem syland

Step	Hyp	Ref	Expression
1		syland.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syland.2	. . . 4 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	expd 420	. . 3 ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))
4	1, 3	syld 47	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))
5	4	impd 415	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sylani  607  sylan2d  608  syl2and  611  onfununi  7989  lt2add  11156  nn0seqcvgd  15959  1stcelcls  22154  llyidm  22181  filuni  22578  ballotlemimin  31984  btwnintr  33863  ifscgr  33888  btwnconn1lem12  33942  poimir  35363  cvrntr  36994  goldbachthlem2  44424