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

Theorem e1a 37000
Description: A Virtual deduction elimination rule. syl 17 is e1a 37000 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 36935 . . 3  |-  ( ph  ->  ps )
3 e1a.2 . . 3  |-  ( ps 
->  ch )
42, 3syl 17 . 2  |-  ( ph  ->  ch )
54dfvd1ir 36937 1  |-  (. ph  ->.  ch
).
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36933
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 189  df-vd1 36934
This theorem is referenced by:  e1bi  37002  e1bir  37003  snelpwrVD  37221  unipwrVD  37222  sstrALT2VD  37224  elex2VD  37228  elex22VD  37229  eqsbc3rVD  37230  zfregs2VD  37231  tpid3gVD  37232  en3lplem1VD  37233  en3lpVD  37235  3ornot23VD  37237  3orbi123VD  37240  sbc3orgVD  37241  exbirVD  37243  3impexpVD  37246  3impexpbicomVD  37247  sbcoreleleqVD  37250  tratrbVD  37252  al2imVD  37253  syl5impVD  37254  ssralv2VD  37257  ordelordALTVD  37258  sbcim2gVD  37266  trsbcVD  37268  truniALTVD  37269  trintALTVD  37271  undif3VD  37273  sbcssgVD  37274  csbingVD  37275  onfrALTlem3VD  37278  simplbi2comtVD  37279  onfrALTlem2VD  37280  onfrALTVD  37282  csbeq2gVD  37283  csbsngVD  37284  csbxpgVD  37285  csbresgVD  37286  csbrngVD  37287  csbima12gALTVD  37288  csbunigVD  37289  csbfv12gALTVD  37290  con5VD  37291  relopabVD  37292  19.41rgVD  37293  2pm13.193VD  37294  hbimpgVD  37295  hbalgVD  37296  hbexgVD  37297  ax6e2eqVD  37298  ax6e2ndVD  37299  ax6e2ndeqVD  37300  2sb5ndVD  37301  2uasbanhVD  37302  e2ebindVD  37303  sb5ALTVD  37304  vk15.4jVD  37305  notnot2ALTVD  37306  con3ALTVD  37307
  Copyright terms: Public domain W3C validator