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

Theorem ee222 28646
Description: e222 28799 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 420 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
3 ee222.2 . . . 4  |-  ( ph  ->  ( ps  ->  th )
)
43imp 420 . . 3  |-  ( (
ph  /\  ps )  ->  th )
5 ee222.3 . . . 4  |-  ( ph  ->  ( ps  ->  ta ) )
65imp 420 . . 3  |-  ( (
ph  /\  ps )  ->  ta )
7 ee222.4 . . 3  |-  ( ch 
->  ( th  ->  ( ta  ->  et ) ) )
82, 4, 6, 7syl3c 60 . 2  |-  ( (
ph  /\  ps )  ->  et )
98ex 425 1  |-  ( ph  ->  ( ps  ->  et ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  ee121  28649  ee122  28650  tratrb  28682  ee220  28801  ee202  28803  ee022  28805  ee002  28807  ee020  28809  ee200  28811  ee221  28813  ee212  28815  ee112  28818  ee211  28821  ee210  28823  ee201  28825  ee120  28827  ee021  28829  ee012  28831  ee102  28833  suctrALT2  29011
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 179  df-an 362
  Copyright terms: Public domain W3C validator