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

Theorem e222 36446
Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e222.1  |-  (. ph ,. ps  ->.  ch ).
e222.2  |-  (. ph ,. ps  ->.  th ).
e222.3  |-  (. ph ,. ps  ->.  ta ).
e222.4  |-  ( ch 
->  ( th  ->  ( ta  ->  et ) ) )
Assertion
Ref Expression
e222  |-  (. ph ,. ps  ->.  et ).

Proof of Theorem e222
StepHypRef Expression
1 e222.3 . . . . . . 7  |-  (. ph ,. ps  ->.  ta ).
21dfvd2i 36386 . . . . . 6  |-  ( ph  ->  ( ps  ->  ta ) )
32imp 427 . . . . 5  |-  ( (
ph  /\  ps )  ->  ta )
4 e222.1 . . . . . . . . 9  |-  (. ph ,. ps  ->.  ch ).
54dfvd2i 36386 . . . . . . . 8  |-  ( ph  ->  ( ps  ->  ch ) )
65imp 427 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ch )
7 e222.2 . . . . . . . . 9  |-  (. ph ,. ps  ->.  th ).
87dfvd2i 36386 . . . . . . . 8  |-  ( ph  ->  ( ps  ->  th )
)
98imp 427 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  th )
10 e222.4 . . . . . . 7  |-  ( ch 
->  ( th  ->  ( ta  ->  et ) ) )
116, 9, 10syl2im 36 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  ->  ( ta 
->  et ) ) )
1211pm2.43i 46 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ta  ->  et ) )
133, 12syl5com 28 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  ->  et ) )
1413pm2.43i 46 . . 3  |-  ( (
ph  /\  ps )  ->  et )
1514ex 432 . 2  |-  ( ph  ->  ( ps  ->  et ) )
1615dfvd2ir 36387 1  |-  (. ph ,. ps  ->.  et ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367   (.wvd2 36378
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 185  df-an 369  df-vd2 36379
This theorem is referenced by:  e220  36447  e202  36449  e022  36451  e002  36453  e020  36455  e200  36457  e221  36459  e212  36461  e122  36463  e112  36464  e121  36466  e211  36467  e22  36481  suctrALT2VD  36666  en3lplem2VD  36674  19.21a3con13vVD  36682  tratrbVD  36692
  Copyright terms: Public domain W3C validator