Theorem syland 615

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 421	. . 3 ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))
4	1, 3	syld 48	. 2 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))
5	4	impd 416	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:  sylani  616  sylan2d  617  syl2and  620  onfununi  8333  fodomfir  9303  lt2add  11782  nn0seqcvgd  16725  1stcelcls  23760  llyidm  23787  filuni  24184  ballotlemimin  35121  rankfilimb  35707  btwnintr  36754  ifscgr  36779  btwnconn1lem12  36833  poimir  38539  cvrntr  40450  goldbachthlem2  48575