Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eel00000 Structured version   Unicode version

Theorem eel00000 36507
Description: Elimination rule similar eel0000 36504, except with five hpothesis steps (Contributed by Alan Sare, 17-Oct-2017.)
Hypotheses
Ref Expression
eel00000.1  |-  ph
eel00000.2  |-  ps
eel00000.3  |-  ch
eel00000.4  |-  th
eel00000.5  |-  ta
eel00000.6  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  et )
Assertion
Ref Expression
eel00000  |-  et

Proof of Theorem eel00000
StepHypRef Expression
1 eel00000.4 . 2  |-  th
2 eel00000.5 . 2  |-  ta
3 eel00000.2 . . 3  |-  ps
4 eel00000.3 . . 3  |-  ch
5 eel00000.1 . . . 4  |-  ph
6 eel00000.6 . . . . 5  |-  ( ( ( ( ( ph  /\ 
ps )  /\  ch )  /\  th )  /\  ta )  ->  et )
76exp41 608 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ch  ->  ( th  ->  ( ta  ->  et ) ) ) )
85, 7mpan 668 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ( ta  ->  et ) ) ) )
93, 4, 8mp2 9 . 2  |-  ( th 
->  ( ta  ->  et ) )
101, 2, 9mp2 9 1  |-  et
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator