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

Metamath Proof Explorer

Theorem eelT01

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

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

Proof

Step Hyp Ref Expression
1 eelT01.1 ⊢ ⊤ → φ
2 eelT01.2 ⊢ ψ
3 eelT01.3 ⊢ χ → θ
4 eelT01.4 ⊢ φ ∧ ψ ∧ θ → τ
5 3anass ⊢ ⊤ ∧ ψ ∧ χ ↔ ⊤ ∧ ψ ∧ χ
6 truan ⊢ ⊤ ∧ ψ ∧ χ ↔ ψ ∧ χ
7 simpr ⊢ ψ ∧ χ → χ
8 2 jctl ⊢ χ → ψ ∧ χ
9 7 8 impbii ⊢ ψ ∧ χ ↔ χ
10 5 6 9 3bitri ⊢ ⊤ ∧ ψ ∧ χ ↔ χ
11 1 4 syl3an1 ⊢ ⊤ ∧ ψ ∧ θ → τ
12 3 11 syl3an3 ⊢ ⊤ ∧ ψ ∧ χ → τ
13 10 12 sylbir ⊢ χ → τ