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 θ