Theorem syland 603

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 415	. . 3 ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))
4	1, 3	syld 47	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))
5	4	impd 410	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:  sylani  604  sylan2d  605  syl2and  608  onfununi  8313  fodomfir  9286  lt2add  11670  nn0seqcvgd  16547  1stcelcls  23355  llyidm  23382  filuni  23779  ballotlemimin  34504  btwnintr  36014  ifscgr  36039  btwnconn1lem12  36093  poimir  37654  cvrntr  39426  goldbachthlem2  47551