Metamath Proof Explorer


Theorem eelT01

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

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

Proof

Step Hyp Ref Expression
1 eelT01.1
 |-  ( T. -> ph )
2 eelT01.2
 |-  ps
3 eelT01.3
 |-  ( ch -> th )
4 eelT01.4
 |-  ( ( ph /\ ps /\ th ) -> ta )
5 3anass
 |-  ( ( T. /\ ps /\ ch ) <-> ( T. /\ ( ps /\ ch ) ) )
6 truan
 |-  ( ( T. /\ ( ps /\ ch ) ) <-> ( ps /\ ch ) )
7 simpr
 |-  ( ( ps /\ ch ) -> ch )
8 2 jctl
 |-  ( ch -> ( ps /\ ch ) )
9 7 8 impbii
 |-  ( ( ps /\ ch ) <-> ch )
10 5 6 9 3bitri
 |-  ( ( T. /\ ps /\ ch ) <-> ch )
11 1 4 syl3an1
 |-  ( ( T. /\ ps /\ th ) -> ta )
12 3 11 syl3an3
 |-  ( ( T. /\ ps /\ ch ) -> ta )
13 10 12 sylbir
 |-  ( ch -> ta )