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

Theorem e222 28799
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 28739 . . . . . 6  |-  ( ph  ->  ( ps  ->  ta ) )
32imp 420 . . . . 5  |-  ( (
ph  /\  ps )  ->  ta )
4 e222.1 . . . . . . . . 9  |-  (. ph ,. ps  ->.  ch ).
54dfvd2i 28739 . . . . . . . 8  |-  ( ph  ->  ( ps  ->  ch ) )
65imp 420 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ch )
7 e222.2 . . . . . . . . 9  |-  (. ph ,. ps  ->.  th ).
87dfvd2i 28739 . . . . . . . 8  |-  ( ph  ->  ( ps  ->  th )
)
98imp 420 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  th )
10 e222.4 . . . . . . 7  |-  ( ch 
->  ( th  ->  ( ta  ->  et ) ) )
116, 9, 10syl2im 37 . . . . . 6  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  ->  ( ta 
->  et ) ) )
1211pm2.43i 46 . . . . 5  |-  ( (
ph  /\  ps )  ->  ( ta  ->  et ) )
133, 12syl5com 29 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  ->  et ) )
1413pm2.43i 46 . . 3  |-  ( (
ph  /\  ps )  ->  et )
1514ex 425 . 2  |-  ( ph  ->  ( ps  ->  et ) )
1615dfvd2ir 28740 1  |-  (. ph ,. ps  ->.  et ).
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   (.wvd2 28731
This theorem is referenced by:  e220  28800  e202  28802  e022  28804  e002  28806  e020  28808  e200  28810  e221  28812  e212  28814  e122  28816  e112  28817  e121  28819  e211  28820  e22  28834  suctrALT2VD  29010  en3lplem2VD  29018  19.21a3con13vVD  29026  tratrbVD  29035
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 179  df-an 362  df-vd2 28732
  Copyright terms: Public domain W3C validator