Metamath Proof Explorer

Theorem eelTTT

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

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

Proof

Step Hyp Ref Expression
1 eelTTT.1 ⊢ ⊤ → φ
2 eelTTT.2 ⊢ ⊤ → ψ
3 eelTTT.3 ⊢ ⊤ → χ
4 eelTTT.4 ⊢ φ ∧ ψ ∧ χ → θ
5 truan ⊢ ⊤ ∧ χ ↔ χ
6 3anass ⊢ ⊤ ∧ ψ ∧ χ ↔ ⊤ ∧ ψ ∧ χ
7 truan ⊢ ⊤ ∧ ψ ∧ χ ↔ ψ ∧ χ
8 6 7 bitri ⊢ ⊤ ∧ ψ ∧ χ ↔ ψ ∧ χ
9 1 4 syl3an1 ⊢ ⊤ ∧ ψ ∧ χ → θ
10 8 9 sylbir ⊢ ψ ∧ χ → θ
11 2 10 sylan ⊢ ⊤ ∧ χ → θ
12 5 11 sylbir ⊢ χ → θ
13 3 12 syl ⊢ ⊤ → θ
14 13 mptru ⊢ θ