Metamath Proof Explorer

Theorem eelT11

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

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

Proof

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