This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eel0TT

Description: An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses eel0TT.1 ⊢ φ
eel0TT.2 ⊢ ⊤ → ψ
eel0TT.3 ⊢ ⊤ → χ
eel0TT.4 ⊢ φ ∧ ψ ∧ χ → θ
Assertion eel0TT ⊢ θ

Proof

Step Hyp Ref Expression
1 eel0TT.1 ⊢ φ
2 eel0TT.2 ⊢ ⊤ → ψ
3 eel0TT.3 ⊢ ⊤ → χ
4 eel0TT.4 ⊢ φ ∧ ψ ∧ χ → θ
5 truan ⊢ ⊤ ∧ χ ↔ χ
6 1 4 mp3an1 ⊢ ψ ∧ χ → θ
7 2 6 sylan ⊢ ⊤ ∧ χ → θ
8 5 7 sylbir ⊢ χ → θ
9 3 8 syl ⊢ ⊤ → θ
10 9 mptru ⊢ θ