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

Metamath Proof Explorer

Theorem eel000cT

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

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

Proof

Step Hyp Ref Expression
1 eel000cT.1 ⊢ φ
2 eel000cT.2 ⊢ ψ
3 eel000cT.3 ⊢ χ
4 eel000cT.4 ⊢ φ ∧ ψ ∧ χ → θ
5 1 4 mp3an1 ⊢ ψ ∧ χ → θ
6 2 5 mpan ⊢ χ → θ
7 3 6 ax-mp ⊢ θ
8 7 a1i ⊢ ⊤ → θ