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

Theorem ee222 27636
Description: e222 27781 without virtual deduction connectives. Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 7-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
ee222.1  |-  ( ph  ->  ( ps  ->  ch ) )
ee222.2  |-  ( ph  ->  ( ps  ->  th )
)
ee222.3  |-  ( ph  ->  ( ps  ->  ta ) )
ee222.4  |-  ( ch 
->  ( th  ->  ( ta  ->  et ) ) )
Assertion
Ref Expression
ee222  |-  ( ph  ->  ( ps  ->  et ) )

Proof of Theorem ee222
StepHypRef Expression
1 ee222.1 . . . 4  |-  ( ph  ->  ( ps  ->  ch ) )
21imp 418 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
3 ee222.2 . . . 4  |-  ( ph  ->  ( ps  ->  th )
)
43imp 418 . . 3  |-  ( (
ph  /\  ps )  ->  th )
5 ee222.3 . . . 4  |-  ( ph  ->  ( ps  ->  ta ) )
65imp 418 . . 3  |-  ( (
ph  /\  ps )  ->  ta )
7 ee222.4 . . 3  |-  ( ch 
->  ( th  ->  ( ta  ->  et ) ) )
82, 4, 6, 7syl3c 57 . 2  |-  ( (
ph  /\  ps )  ->  et )
98ex 423 1  |-  ( ph  ->  ( ps  ->  et ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ee121  27639  ee122  27640  tratrb  27672  ee220  27783  ee202  27785  ee022  27787  ee002  27789  ee020  27791  ee200  27793  ee221  27795  ee212  27797  ee112  27800  ee211  27803  ee210  27805  ee201  27807  ee120  27809  ee021  27811  ee012  27813  ee102  27815  suctrALT2  27986
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator