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

Theorem e222 28408
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 28354 . . . . . 6  |-  ( ph  ->  ( ps  ->  ta ) )
32imp 418 . . . . 5  |-  ( (
ph  /\  ps )  ->  ta )
4 e222.1 . . . . . . . . 9  |-  (. ph ,. ps  ->.  ch ).
54dfvd2i 28354 . . . . . . . 8  |-  ( ph  ->  ( ps  ->  ch ) )
65imp 418 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ch )
7 e222.2 . . . . . . . . 9  |-  (. ph ,. ps  ->.  th ).
87dfvd2i 28354 . . . . . . . 8  |-  ( ph  ->  ( ps  ->  th )
)
98imp 418 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  th )
10 e222.4 . . . . . . 7  |-  ( ch 
->  ( th  ->  ( ta  ->  et ) ) )
116, 9, 10syl2im 34 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  ->  ( ta 
->  et ) ) )
1211pm2.43i 43 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ta  ->  et ) )
133, 12syl5com 26 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  ->  et ) )
1413pm2.43i 43 . . 3  |-  ( (
ph  /\  ps )  ->  et )
1514ex 423 . 2  |-  ( ph  ->  ( ps  ->  et ) )
1615dfvd2ir 28355 1  |-  (. ph ,. ps  ->.  et ).
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   (.wvd2 28346
This theorem is referenced by:  e220  28409  e202  28411  e022  28413  e002  28415  e020  28417  e200  28419  e221  28421  e212  28423  e122  28425  e112  28426  e121  28428  e211  28429  e22  28443  suctrALT2VD  28612  en3lplem2VD  28620  19.21a3con13vVD  28628  tratrbVD  28637
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-vd2 28347
  Copyright terms: Public domain W3C validator