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  8352  fodomfir  9322  lt2add  11804  nn0seqcvgd  16750  1stcelcls  23785  llyidm  23812  filuni  24209  ballotlemimin  35184  rankfilimb  35780  btwnintr  36876  ifscgr  36901  btwnconn1lem12  36955  poimir  38664  cvrntr  40575  goldbachthlem2  48724