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

Metamath Proof Explorer

Theorem eelTTT

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

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

Proof

Step Hyp Ref Expression
1 eelTTT.1 
 |-  ( T. -> ph )
2 eelTTT.2 
 |-  ( T. -> ps )
3 eelTTT.3 
 |-  ( T. -> ch )
4 eelTTT.4 
 |-  ( ( ph /\ ps /\ ch ) -> th )
5 truan 
 |-  ( ( T. /\ ch ) <-> ch )
6 3anass 
 |-  ( ( T. /\ ps /\ ch ) <-> ( T. /\ ( ps /\ ch ) ) )
7 truan 
 |-  ( ( T. /\ ( ps /\ ch ) ) <-> ( ps /\ ch ) )
8 6 7 bitri 
 |-  ( ( T. /\ ps /\ ch ) <-> ( ps /\ ch ) )
9 1 4 syl3an1 
 |-  ( ( T. /\ ps /\ ch ) -> th )
10 8 9 sylbir 
 |-  ( ( ps /\ ch ) -> th )
11 2 10 sylan 
 |-  ( ( T. /\ ch ) -> th )
12 5 11 sylbir 
 |-  ( ch -> th )
13 3 12 syl 
 |-  ( T. -> th )
14 13 mptru 
 |-  th