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

Theorem ee222 28295
Description: e222 28446 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 419 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
3 ee222.2 . . . 4  |-  ( ph  ->  ( ps  ->  th )
)
43imp 419 . . 3  |-  ( (
ph  /\  ps )  ->  th )
5 ee222.3 . . . 4  |-  ( ph  ->  ( ps  ->  ta ) )
65imp 419 . . 3  |-  ( (
ph  /\  ps )  ->  ta )
7 ee222.4 . . 3  |-  ( ch 
->  ( th  ->  ( ta  ->  et ) ) )
82, 4, 6, 7syl3c 59 . 2  |-  ( (
ph  /\  ps )  ->  et )
98ex 424 1  |-  ( ph  ->  ( ps  ->  et ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  ee121  28298  ee122  28299  tratrb  28331  ee220  28448  ee202  28450  ee022  28452  ee002  28454  ee020  28456  ee200  28458  ee221  28460  ee212  28462  ee112  28465  ee211  28468  ee210  28470  ee201  28472  ee120  28474  ee021  28476  ee012  28478  ee102  28480  suctrALT2  28658
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 178  df-an 361
  Copyright terms: Public domain W3C validator