This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eel0T1

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

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

Proof

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