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

Theorem e1a 32786
Description: A Virtual deduction elimination rule. syl 16 is e1a 32786 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 32721 . . 3  |-  ( ph  ->  ps )
3 e1a.2 . . 3  |-  ( ps 
->  ch )
42, 3syl 16 . 2  |-  ( ph  ->  ch )
54dfvd1ir 32723 1  |-  (. ph  ->.  ch
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 32719
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 32720
This theorem is referenced by:  e1bi  32788  e1bir  32789  snelpwrVD  33004  unipwrVD  33005  sstrALT2VD  33007  elex2VD  33011  elex22VD  33012  eqsbc3rVD  33013  zfregs2VD  33014  tpid3gVD  33015  en3lplem1VD  33016  en3lpVD  33018  3ornot23VD  33020  3orbi123VD  33023  sbc3orgVD  33024  exbirVD  33026  3impexpVD  33029  3impexpbicomVD  33030  sbcoreleleqVD  33032  tratrbVD  33034  3ax4VD  33035  syl5impVD  33036  ssralv2VD  33039  ordelordALTVD  33040  sbcim2gVD  33048  trsbcVD  33050  truniALTVD  33051  trintALTVD  33053  undif3VD  33055  sbcssgVD  33056  csbingVD  33057  onfrALTlem3VD  33060  simplbi2comtVD  33061  onfrALTlem2VD  33062  onfrALTVD  33064  csbeq2gVD  33065  csbsngVD  33066  csbxpgVD  33067  csbresgVD  33068  csbrngVD  33069  csbima12gALTVD  33070  csbunigVD  33071  csbfv12gALTVD  33072  con5VD  33073  relopabVD  33074  19.41rgVD  33075  2pm13.193VD  33076  hbimpgVD  33077  hbalgVD  33078  hbexgVD  33079  ax6e2eqVD  33080  ax6e2ndVD  33081  ax6e2ndeqVD  33082  2sb5ndVD  33083  2uasbanhVD  33084  e2ebindVD  33085  sb5ALTVD  33086  vk15.4jVD  33087  notnot2ALTVD  33088  con3ALTVD  33089
  Copyright terms: Public domain W3C validator