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

Metamath Proof Explorer

Theorem eelT11

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

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

Proof

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