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

Theorem e222 31710
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 31650 . . . . . 6  |-  ( ph  ->  ( ps  ->  ta ) )
32imp 429 . . . . 5  |-  ( (
ph  /\  ps )  ->  ta )
4 e222.1 . . . . . . . . 9  |-  (. ph ,. ps  ->.  ch ).
54dfvd2i 31650 . . . . . . . 8  |-  ( ph  ->  ( ps  ->  ch ) )
65imp 429 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ch )
7 e222.2 . . . . . . . . 9  |-  (. ph ,. ps  ->.  th ).
87dfvd2i 31650 . . . . . . . 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 31651 1  |-  (. ph ,. ps  ->.  et ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   (.wvd2 31642
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 31643
This theorem is referenced by:  e220  31711  e202  31713  e022  31715  e002  31717  e020  31719  e200  31721  e221  31723  e212  31725  e122  31727  e112  31728  e121  31730  e211  31731  e22  31745  suctrALT2VD  31924  en3lplem2VD  31932  19.21a3con13vVD  31940  tratrbVD  31949
  Copyright terms: Public domain W3C validator