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

Theorem e12 37107
Description: A virtual deduction elimination rule (see sylsyld 58). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e12.1  |-  (. ph  ->.  ps
).
e12.2  |-  (. ph ,. ch  ->.  th ).
e12.3  |-  ( ps 
->  ( th  ->  ta ) )
Assertion
Ref Expression
e12  |-  (. ph ,. ch  ->.  ta ).

Proof of Theorem e12
StepHypRef Expression
1 e12.1 . . 3  |-  (. ph  ->.  ps
).
21vd12 36978 . 2  |-  (. ph ,. ch  ->.  ps ).
3 e12.2 . 2  |-  (. ph ,. ch  ->.  th ).
4 e12.3 . 2  |-  ( ps 
->  ( th  ->  ta ) )
52, 3, 4e22 37049 1  |-  (. ph ,. ch  ->.  ta ).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36938   (.wvd2 36946
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 190  df-an 377  df-vd1 36939  df-vd2 36947
This theorem is referenced by:  e12an  37108  trsspwALT  37202  sspwtr  37205  pwtrVD  37216  snssiALTVD  37219  elex2VD  37230  elex22VD  37231  eqsbc3rVD  37232  en3lplem1VD  37235  3ornot23VD  37239  orbi1rVD  37240  19.21a3con13vVD  37244  exbirVD  37245  tratrbVD  37254  ssralv2VD  37259  sbcim2gVD  37268  sbcbiVD  37269  relopabVD  37294  19.41rgVD  37295  ax6e2eqVD  37300  ax6e2ndeqVD  37302  vk15.4jVD  37307  con3ALTVD  37309
  Copyright terms: Public domain W3C validator