Metamath Proof Explorer

Theorem eel0T1

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

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

Proof

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