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

Theorem in1 33216
Description: Inference form of df-vd1 33215. 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  |-  (. ph  ->.  ps
).
Assertion
Ref Expression
in1  |-  ( ph  ->  ps )

Proof of Theorem in1
StepHypRef Expression
1 in1.1 . 2  |-  (. ph  ->.  ps
).
2 df-vd1 33215 . 2  |-  ( (.
ph 
->.  ps ).  <->  ( ph  ->  ps ) )
31, 2mpbi 208 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 33214
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 33215
This theorem is referenced by:  vd12  33254  vd13  33255  gen11nv  33271  gen12  33272  exinst11  33280  e1a  33281  el1  33282  e223  33289  e111  33328  e1111  33329  el2122old  33382  el12  33391  el123  33429  un0.1  33444  trsspwALT  33484  sspwtr  33487  pwtrVD  33492  pwtrrVD  33493  snssiALTVD  33495  snsslVD  33497  snelpwrVD  33499  unipwrVD  33500  sstrALT2VD  33502  suctrALT2VD  33504  elex2VD  33506  elex22VD  33507  eqsbc3rVD  33508  zfregs2VD  33509  tpid3gVD  33510  en3lplem1VD  33511  en3lplem2VD  33512  en3lpVD  33513  3ornot23VD  33515  orbi1rVD  33516  3orbi123VD  33518  sbc3orgVD  33519  19.21a3con13vVD  33520  exbirVD  33521  exbiriVD  33522  rspsbc2VD  33523  3impexpVD  33524  3impexpbicomVD  33525  sbcoreleleqVD  33527  tratrbVD  33529  al2imVD  33530  syl5impVD  33531  ssralv2VD  33534  ordelordALTVD  33535  equncomVD  33536  imbi12VD  33541  imbi13VD  33542  sbcim2gVD  33543  sbcbiVD  33544  trsbcVD  33545  truniALTVD  33546  trintALTVD  33548  undif3VD  33550  sbcssgVD  33551  csbingVD  33552  simplbi2comtVD  33556  onfrALTVD  33559  csbeq2gVD  33560  csbsngVD  33561  csbxpgVD  33562  csbresgVD  33563  csbrngVD  33564  csbima12gALTVD  33565  csbunigVD  33566  csbfv12gALTVD  33567  con5VD  33568  relopabVD  33569  19.41rgVD  33570  2pm13.193VD  33571  hbimpgVD  33572  hbalgVD  33573  hbexgVD  33574  ax6e2eqVD  33575  ax6e2ndVD  33576  ax6e2ndeqVD  33577  2sb5ndVD  33578  2uasbanhVD  33579  e2ebindVD  33580  sb5ALTVD  33581  vk15.4jVD  33582  notnot2ALTVD  33583  con3ALTVD  33584  sspwimpVD  33587  sspwimpcfVD  33589  suctrALTcfVD  33591
  Copyright terms: Public domain W3C validator