Theorem syland 614

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 48	. 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  615  sylan2d  616  syl2and  619  onfununi  8316  fodomfir  9275  lt2add  11687  nn0seqcvgd  16618  1stcelcls  23579  llyidm  23606  filuni  24003  ballotlemimin  34813  rankfilimb  35410  btwnintr  36382  ifscgr  36407  btwnconn1lem12  36461  poimir  38164  cvrntr  40061  goldbachthlem2  48153