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

Theorem ee222 36543
Description: e222 36701 without virtual deduction connectives. Special theorem needed for the 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 430 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
3 ee222.2 . . . 4  |-  ( ph  ->  ( ps  ->  th )
)
43imp 430 . . 3  |-  ( (
ph  /\  ps )  ->  th )
5 ee222.3 . . . 4  |-  ( ph  ->  ( ps  ->  ta ) )
65imp 430 . . 3  |-  ( (
ph  /\  ps )  ->  ta )
7 ee222.4 . . 3  |-  ( ch 
->  ( th  ->  ( ta  ->  et ) ) )
82, 4, 6, 7syl3c 63 . 2  |-  ( (
ph  /\  ps )  ->  et )
98ex 435 1  |-  ( ph  ->  ( ps  ->  et ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  ee121  36546  ee122  36547  tratrb  36582  ee220  36703  ee202  36705  ee022  36707  ee002  36709  ee020  36711  ee200  36713  ee221  36715  ee212  36717  ee112  36720  ee211  36723  ee210  36725  ee201  36727  ee120  36729  ee021  36731  ee012  36733  ee102  36735  suctrALT2  36921
  Copyright terms: Public domain W3C validator