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
|- ph
eel000cT.2
|- ps
eel000cT.3
|- ch
eel000cT.4
|- ( ( ph /\ ps /\ ch ) -> th )
Assertion eel000cT
|- ( T. -> th )

Proof

Step Hyp Ref Expression
1 eel000cT.1
 |-  ph
2 eel000cT.2
 |-  ps
3 eel000cT.3
 |-  ch
4 eel000cT.4
 |-  ( ( ph /\ ps /\ ch ) -> th )
5 1 4 mp3an1
 |-  ( ( ps /\ ch ) -> th )
6 2 5 mpan
 |-  ( ch -> th )
7 3 6 ax-mp
 |-  th
8 7 a1i
 |-  ( T. -> th )