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

Theorem e1a 33121
Description: A Virtual deduction elimination rule. syl 16 is e1a 33121 without virtual deductions. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
e1a.1  |-  (. ph  ->.  ps
).
e1a.2  |-  ( ps 
->  ch )
Assertion
Ref Expression
e1a  |-  (. ph  ->.  ch
).

Proof of Theorem e1a
StepHypRef Expression
1 e1a.1 . . . 4  |-  (. ph  ->.  ps
).
21in1 33056 . . 3  |-  ( ph  ->  ps )
3 e1a.2 . . 3  |-  ( ps 
->  ch )
42, 3syl 16 . 2  |-  ( ph  ->  ch )
54dfvd1ir 33058 1  |-  (. ph  ->.  ch
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 33054
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-vd1 33055
This theorem is referenced by:  e1bi  33123  e1bir  33124  snelpwrVD  33339  unipwrVD  33340  sstrALT2VD  33342  elex2VD  33346  elex22VD  33347  eqsbc3rVD  33348  zfregs2VD  33349  tpid3gVD  33350  en3lplem1VD  33351  en3lpVD  33353  3ornot23VD  33355  3orbi123VD  33358  sbc3orgVD  33359  exbirVD  33361  3impexpVD  33364  3impexpbicomVD  33365  sbcoreleleqVD  33367  tratrbVD  33369  al2imVD  33370  syl5impVD  33371  ssralv2VD  33374  ordelordALTVD  33375  sbcim2gVD  33383  trsbcVD  33385  truniALTVD  33386  trintALTVD  33388  undif3VD  33390  sbcssgVD  33391  csbingVD  33392  onfrALTlem3VD  33395  simplbi2comtVD  33396  onfrALTlem2VD  33397  onfrALTVD  33399  csbeq2gVD  33400  csbsngVD  33401  csbxpgVD  33402  csbresgVD  33403  csbrngVD  33404  csbima12gALTVD  33405  csbunigVD  33406  csbfv12gALTVD  33407  con5VD  33408  relopabVD  33409  19.41rgVD  33410  2pm13.193VD  33411  hbimpgVD  33412  hbalgVD  33413  hbexgVD  33414  ax6e2eqVD  33415  ax6e2ndVD  33416  ax6e2ndeqVD  33417  2sb5ndVD  33418  2uasbanhVD  33419  e2ebindVD  33420  sb5ALTVD  33421  vk15.4jVD  33422  notnot2ALTVD  33423  con3ALTVD  33424
  Copyright terms: Public domain W3C validator