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

Theorem e222 33565
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 33505 . . . . . 6  |-  ( ph  ->  ( ps  ->  ta ) )
32imp 429 . . . . 5  |-  ( (
ph  /\  ps )  ->  ta )
4 e222.1 . . . . . . . . 9  |-  (. ph ,. ps  ->.  ch ).
54dfvd2i 33505 . . . . . . . 8  |-  ( ph  ->  ( ps  ->  ch ) )
65imp 429 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ch )
7 e222.2 . . . . . . . . 9  |-  (. ph ,. ps  ->.  th ).
87dfvd2i 33505 . . . . . . . 8  |-  ( ph  ->  ( ps  ->  th )
)
98imp 429 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  th )
10 e222.4 . . . . . . 7  |-  ( ch 
->  ( th  ->  ( ta  ->  et ) ) )
116, 9, 10syl2im 38 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  ->  ( ta 
->  et ) ) )
1211pm2.43i 47 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ta  ->  et ) )
133, 12syl5com 30 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  ->  et ) )
1413pm2.43i 47 . . 3  |-  ( (
ph  /\  ps )  ->  et )
1514ex 434 . 2  |-  ( ph  ->  ( ps  ->  et ) )
1615dfvd2ir 33506 1  |-  (. ph ,. ps  ->.  et ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   (.wvd2 33497
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 371  df-vd2 33498
This theorem is referenced by:  e220  33566  e202  33568  e022  33570  e002  33572  e020  33574  e200  33576  e221  33578  e212  33580  e122  33582  e112  33583  e121  33585  e211  33586  e22  33600  suctrALT2VD  33779  en3lplem2VD  33787  19.21a3con13vVD  33795  tratrbVD  33804
  Copyright terms: Public domain W3C validator