Theorem eel00001 42341

Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)

Hypotheses

Ref	Expression
eel00001.1	⊢ 𝜑
eel00001.2	⊢ 𝜓
eel00001.3	⊢ 𝜒
eel00001.4	⊢ 𝜃
eel00001.5	⊢ (𝜏 → 𝜂)
eel00001.6	⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜁)

Assertion

Ref	Expression
eel00001	⊢ (𝜏 → 𝜁)

Proof of Theorem eel00001

Step	Hyp	Ref	Expression
1		eel00001.5	. 2 ⊢ (𝜏 → 𝜂)
2		eel00001.3	. . 3 ⊢ 𝜒
3		eel00001.4	. . 3 ⊢ 𝜃
4		eel00001.1	. . . 4 ⊢ 𝜑
5		eel00001.2	. . . 4 ⊢ 𝜓
6		eel00001.6	. . . . 5 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜁)
7	6	exp41 435	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → (𝜂 → 𝜁))))
8	4, 5, 7	mp2an 689	. . 3 ⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁)))
9	2, 3, 8	mp2 9	. 2 ⊢ (𝜂 → 𝜁)
10	1, 9	syl 17	1 ⊢ (𝜏 → 𝜁)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by: (None)