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

Theorem in1 36578
Description: Inference form of df-vd1 36577. 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 36577 . 2  |-  ( (.
ph 
->.  ps ).  <->  ( ph  ->  ps ) )
31, 2mpbi 211 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36576
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 188  df-vd1 36577
This theorem is referenced by:  vd12  36616  vd13  36617  gen11nv  36633  gen12  36634  exinst11  36642  e1a  36643  el1  36644  e223  36651  e111  36690  e1111  36691  el2122old  36743  el12  36752  el123  36790  un0.1  36805  trsspwALT  36845  sspwtr  36848  pwtrVD  36859  pwtrrVD  36860  snssiALTVD  36862  snsslVD  36864  snelpwrVD  36866  unipwrVD  36867  sstrALT2VD  36869  suctrALT2VD  36871  elex2VD  36873  elex22VD  36874  eqsbc3rVD  36875  zfregs2VD  36876  tpid3gVD  36877  en3lplem1VD  36878  en3lplem2VD  36879  en3lpVD  36880  3ornot23VD  36882  orbi1rVD  36883  3orbi123VD  36885  sbc3orgVD  36886  19.21a3con13vVD  36887  exbirVD  36888  exbiriVD  36889  rspsbc2VD  36890  3impexpVD  36891  3impexpbicomVD  36892  sbcoreleleqVD  36895  tratrbVD  36897  al2imVD  36898  syl5impVD  36899  ssralv2VD  36902  ordelordALTVD  36903  equncomVD  36904  imbi12VD  36909  imbi13VD  36910  sbcim2gVD  36911  sbcbiVD  36912  trsbcVD  36913  truniALTVD  36914  trintALTVD  36916  undif3VD  36918  sbcssgVD  36919  csbingVD  36920  simplbi2comtVD  36924  onfrALTVD  36927  csbeq2gVD  36928  csbsngVD  36929  csbxpgVD  36930  csbresgVD  36931  csbrngVD  36932  csbima12gALTVD  36933  csbunigVD  36934  csbfv12gALTVD  36935  con5VD  36936  relopabVD  36937  19.41rgVD  36938  2pm13.193VD  36939  hbimpgVD  36940  hbalgVD  36941  hbexgVD  36942  ax6e2eqVD  36943  ax6e2ndVD  36944  ax6e2ndeqVD  36945  2sb5ndVD  36946  2uasbanhVD  36947  e2ebindVD  36948  sb5ALTVD  36949  vk15.4jVD  36950  notnot2ALTVD  36951  con3ALTVD  36952  sspwimpVD  36955  sspwimpcfVD  36957  suctrALTcfVD  36959
  Copyright terms: Public domain W3C validator