Metamath Proof Explorer


Theorem eel000cT

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

Ref Expression
Hypotheses eel000cT.1 φ
eel000cT.2 ψ
eel000cT.3 χ
eel000cT.4 φ ψ χ θ
Assertion eel000cT θ

Proof

Step Hyp Ref Expression
1 eel000cT.1 φ
2 eel000cT.2 ψ
3 eel000cT.3 χ
4 eel000cT.4 φ ψ χ θ
5 1 4 mp3an1 ψ χ θ
6 2 5 mpan χ θ
7 3 6 ax-mp θ
8 7 a1i θ