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

Theorem in1 36984
Description: Inference form of df-vd1 36983. 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 36983 . 2  |-  ( (.
ph 
->.  ps ).  <->  ( ph  ->  ps ) )
31, 2mpbi 213 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36982
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 190  df-vd1 36983
This theorem is referenced by:  vd12  37022  vd13  37023  gen11nv  37039  gen12  37040  exinst11  37048  e1a  37049  el1  37050  e223  37057  e111  37096  e1111  37097  el2122old  37144  el12  37153  el123  37191  un0.1  37206  trsspwALT  37246  sspwtr  37249  pwtrVD  37260  pwtrrVD  37261  snssiALTVD  37263  snsslVD  37265  snelpwrVD  37267  unipwrVD  37268  sstrALT2VD  37270  suctrALT2VD  37272  elex2VD  37274  elex22VD  37275  eqsbc3rVD  37276  zfregs2VD  37277  tpid3gVD  37278  en3lplem1VD  37279  en3lplem2VD  37280  en3lpVD  37281  3ornot23VD  37283  orbi1rVD  37284  3orbi123VD  37286  sbc3orgVD  37287  19.21a3con13vVD  37288  exbirVD  37289  exbiriVD  37290  rspsbc2VD  37291  3impexpVD  37292  3impexpbicomVD  37293  sbcoreleleqVD  37296  tratrbVD  37298  al2imVD  37299  syl5impVD  37300  ssralv2VD  37303  ordelordALTVD  37304  equncomVD  37305  imbi12VD  37310  imbi13VD  37311  sbcim2gVD  37312  sbcbiVD  37313  trsbcVD  37314  truniALTVD  37315  trintALTVD  37317  undif3VD  37319  sbcssgVD  37320  csbingVD  37321  simplbi2comtVD  37325  onfrALTVD  37328  csbeq2gVD  37329  csbsngVD  37330  csbxpgVD  37331  csbresgVD  37332  csbrngVD  37333  csbima12gALTVD  37334  csbunigVD  37335  csbfv12gALTVD  37336  con5VD  37337  relopabVD  37338  19.41rgVD  37339  2pm13.193VD  37340  hbimpgVD  37341  hbalgVD  37342  hbexgVD  37343  ax6e2eqVD  37344  ax6e2ndVD  37345  ax6e2ndeqVD  37346  2sb5ndVD  37347  2uasbanhVD  37348  e2ebindVD  37349  sb5ALTVD  37350  vk15.4jVD  37351  notnot2ALTVD  37352  con3ALTVD  37353  sspwimpVD  37356  sspwimpcfVD  37358  suctrALTcfVD  37360
  Copyright terms: Public domain W3C validator