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

Theorem e222 36874
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 36814 . . . . . 6  |-  ( ph  ->  ( ps  ->  ta ) )
32imp 430 . . . . 5  |-  ( (
ph  /\  ps )  ->  ta )
4 e222.1 . . . . . . . . 9  |-  (. ph ,. ps  ->.  ch ).
54dfvd2i 36814 . . . . . . . 8  |-  ( ph  ->  ( ps  ->  ch ) )
65imp 430 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ch )
7 e222.2 . . . . . . . . 9  |-  (. ph ,. ps  ->.  th ).
87dfvd2i 36814 . . . . . . . 8  |-  ( ph  ->  ( ps  ->  th )
)
98imp 430 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  th )
10 e222.4 . . . . . . 7  |-  ( ch 
->  ( th  ->  ( ta  ->  et ) ) )
116, 9, 10syl2im 39 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  ->  ( ta 
->  et ) ) )
1211pm2.43i 49 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ta  ->  et ) )
133, 12syl5com 31 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  ->  et ) )
1413pm2.43i 49 . . 3  |-  ( (
ph  /\  ps )  ->  et )
1514ex 435 . 2  |-  ( ph  ->  ( ps  ->  et ) )
1615dfvd2ir 36815 1  |-  (. ph ,. ps  ->.  et ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   (.wvd2 36806
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  df-vd2 36807
This theorem is referenced by:  e220  36875  e202  36877  e022  36879  e002  36881  e020  36883  e200  36885  e221  36887  e212  36889  e122  36891  e112  36892  e121  36894  e211  36895  e22  36909  suctrALT2VD  37093  en3lplem2VD  37101  19.21a3con13vVD  37109  tratrbVD  37119
  Copyright terms: Public domain W3C validator