Metamath Proof Explorer


Theorem eelT00

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

Ref Expression
Hypotheses eelT00.1
|- ( T. -> ph )
eelT00.2
|- ps
eelT00.3
|- ch
eelT00.4
|- ( ( ph /\ ps /\ ch ) -> th )
Assertion eelT00
|- th

Proof

Step Hyp Ref Expression
1 eelT00.1
 |-  ( T. -> ph )
2 eelT00.2
 |-  ps
3 eelT00.3
 |-  ch
4 eelT00.4
 |-  ( ( ph /\ ps /\ ch ) -> th )
5 3anass
 |-  ( ( T. /\ ps /\ ch ) <-> ( T. /\ ( ps /\ ch ) ) )
6 truan
 |-  ( ( T. /\ ( ps /\ ch ) ) <-> ( ps /\ ch ) )
7 5 6 bitri
 |-  ( ( T. /\ ps /\ ch ) <-> ( ps /\ ch ) )
8 1 4 syl3an1
 |-  ( ( T. /\ ps /\ ch ) -> th )
9 7 8 sylbir
 |-  ( ( ps /\ ch ) -> th )
10 2 9 mpan
 |-  ( ch -> th )
11 3 10 ax-mp
 |-  th