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

Theorem ee222 28562
Description: e222 28713 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  28565  ee122  28566  tratrb  28598  ee220  28715  ee202  28717  ee022  28719  ee002  28721  ee020  28723  ee200  28725  ee221  28727  ee212  28729  ee112  28732  ee211  28735  ee210  28737  ee201  28739  ee120  28741  ee021  28743  ee012  28745  ee102  28747  suctrALT2  28929
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