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

Metamath Proof Explorer

Theorem eelT00

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

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

Proof

Step Hyp Ref Expression
1 eelT00.1 ⊢ ⊤ → φ
2 eelT00.2 ⊢ ψ
3 eelT00.3 ⊢ χ
4 eelT00.4 ⊢ φ ∧ ψ ∧ χ → θ
5 3anass ⊢ ⊤ ∧ ψ ∧ χ ↔ ⊤ ∧ ψ ∧ χ
6 truan ⊢ ⊤ ∧ ψ ∧ χ ↔ ψ ∧ χ
7 5 6 bitri ⊢ ⊤ ∧ ψ ∧ χ ↔ ψ ∧ χ
8 1 4 syl3an1 ⊢ ⊤ ∧ ψ ∧ χ → θ
9 7 8 sylbir ⊢ ψ ∧ χ → θ
10 2 9 mpan ⊢ χ → θ
11 3 10 ax-mp ⊢ θ