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

Theorem in1 30861
Description: Inference form of df-vd1 30860. 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 30860 . 2
31, 2mpbi 202 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  (.wvd1 30859
This theorem is referenced by:  vd12  30900  vd13  30901  gen11nv  30917  gen12  30918  exinst11  30926  e1_  30927  el1  30928  e223  30935  e111  30974  e1111  30975  el2122old  31028  el12  31037  el123  31075  un0.1  31090  trsspwALT  31130  sspwtr  31133  pwtrVD  31138  pwtrrVD  31139  snssiALTVD  31141  snsslVD  31143  snelpwrVD  31145  unipwrVD  31146  sstrALT2VD  31148  suctrALT2VD  31150  elex2VD  31152  elex22VD  31153  eqsbc3rVD  31154  zfregs2VD  31155  tpid3gVD  31156  en3lplem1VD  31157  en3lplem2VD  31158  en3lpVD  31159  3ornot23VD  31161  orbi1rVD  31162  3orbi123VD  31164  sbc3orgVD  31165  19.21a3con13vVD  31166  exbirVD  31167  exbiriVD  31168  rspsbc2VD  31169  3impexpVD  31170  3impexpbicomVD  31171  sbcoreleleqVD  31173  tratrbVD  31175  3ax4VD  31176  syl5impVD  31177  ssralv2VD  31180  ordelordALTVD  31181  equncomVD  31182  imbi12VD  31187  imbi13VD  31188  sbcim2gVD  31189  sbcbiVD  31190  trsbcVD  31191  truniALTVD  31192  trintALTVD  31194  undif3VD  31196  sbcssgVD  31197  csbingVD  31198  simplbi2comgVD  31202  onfrALTVD  31205  csbeq2gVD  31206  csbsngVD  31207  csbxpgVD  31208  csbresgVD  31209  csbrngVD  31210  csbima12gALTVD  31211  csbunigVD  31212  csbfv12gALTVD  31213  con5VD  31214  relopabVD  31215  19.41rgVD  31216  2pm13.193VD  31217  hbimpgVD  31218  hbalgVD  31219  hbexgVD  31220  ax6e2eqVD  31221  ax6e2ndVD  31222  ax6e2ndeqVD  31223  2sb5ndVD  31224  2uasbanhVD  31225  e2ebindVD  31226  sb5ALTVD  31227  vk15.4jVD  31228  notnot2ALTVD  31229  con3ALTVD  31230  sspwimpVD  31233  sspwimpcfVD  31235  suctrALTcfVD  31237
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 179  df-vd1 30860
  Copyright terms: Public domain W3C validator