Metamath Proof Explorer

Theorem eelTT1

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

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

Proof

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