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

Theorem in1 32127
Description: Inference form of df-vd1 32126. Virtual deduction introduction rule of converting the virtual hypothesis of a 1-virtual hypothesis virtual deduction into an antecedent. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
in1.1
Assertion
Ref Expression
in1

Proof of Theorem in1
StepHypRef Expression
1 in1.1 . 2
2 df-vd1 32126 . 2
31, 2mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  (.wvd1 32125
This theorem is referenced by:  vd12  32165  vd13  32166  gen11nv  32182  gen12  32183  exinst11  32191  e1a  32192  el1  32193  e223  32200  e111  32239  e1111  32240  el2122old  32293  el12  32302  el123  32340  un0.1  32355  trsspwALT  32395  sspwtr  32398  pwtrVD  32403  pwtrrVD  32404  snssiALTVD  32406  snsslVD  32408  snelpwrVD  32410  unipwrVD  32411  sstrALT2VD  32413  suctrALT2VD  32415  elex2VD  32417  elex22VD  32418  eqsbc3rVD  32419  zfregs2VD  32420  tpid3gVD  32421  en3lplem1VD  32422  en3lplem2VD  32423  en3lpVD  32424  3ornot23VD  32426  orbi1rVD  32427  3orbi123VD  32429  sbc3orgVD  32430  19.21a3con13vVD  32431  exbirVD  32432  exbiriVD  32433  rspsbc2VD  32434  3impexpVD  32435  3impexpbicomVD  32436  sbcoreleleqVD  32438  tratrbVD  32440  3ax4VD  32441  syl5impVD  32442  ssralv2VD  32445  ordelordALTVD  32446  equncomVD  32447  imbi12VD  32452  imbi13VD  32453  sbcim2gVD  32454  sbcbiVD  32455  trsbcVD  32456  truniALTVD  32457  trintALTVD  32459  undif3VD  32461  sbcssgVD  32462  csbingVD  32463  simplbi2comtVD  32467  onfrALTVD  32470  csbeq2gVD  32471  csbsngVD  32472  csbxpgVD  32473  csbresgVD  32474  csbrngVD  32475  csbima12gALTVD  32476  csbunigVD  32477  csbfv12gALTVD  32478  con5VD  32479  relopabVD  32480  19.41rgVD  32481  2pm13.193VD  32482  hbimpgVD  32483  hbalgVD  32484  hbexgVD  32485  ax6e2eqVD  32486  ax6e2ndVD  32487  ax6e2ndeqVD  32488  2sb5ndVD  32489  2uasbanhVD  32490  e2ebindVD  32491  sb5ALTVD  32492  vk15.4jVD  32493  notnot2ALTVD  32494  con3ALTVD  32495  sspwimpVD  32498  sspwimpcfVD  32500  suctrALTcfVD  32502
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 32126
  Copyright terms: Public domain W3C validator