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

Theorem e222 28713
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 28653 . . . . . 6  |-  ( ph  ->  ( ps  ->  ta ) )
32imp 418 . . . . 5  |-  ( (
ph  /\  ps )  ->  ta )
4 e222.1 . . . . . . . . 9  |-  (. ph ,. ps  ->.  ch ).
54dfvd2i 28653 . . . . . . . 8  |-  ( ph  ->  ( ps  ->  ch ) )
65imp 418 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ch )
7 e222.2 . . . . . . . . 9  |-  (. ph ,. ps  ->.  th ).
87dfvd2i 28653 . . . . . . . 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 28654 1  |-  (. ph ,. ps  ->.  et ).
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   (.wvd2 28645
This theorem is referenced by:  e220  28714  e202  28716  e022  28718  e002  28720  e020  28722  e200  28724  e221  28726  e212  28728  e122  28730  e112  28731  e121  28733  e211  28734  e22  28748  suctrALT2VD  28928  en3lplem2VD  28936  19.21a3con13vVD  28944  tratrbVD  28953
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 28646
  Copyright terms: Public domain W3C validator