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

Theorem in1 31284
Description: Inference form of df-vd1 31283. 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 31283 . 2  |-  ( (.
ph 
->.  ps ).  <->  ( ph  ->  ps ) )
31, 2mpbi 208 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 31282
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 31283
This theorem is referenced by:  vd12  31322  vd13  31323  gen11nv  31339  gen12  31340  exinst11  31348  e1a  31349  el1  31350  e223  31357  e111  31396  e1111  31397  el2122old  31450  el12  31459  el123  31497  un0.1  31512  trsspwALT  31552  sspwtr  31555  pwtrVD  31560  pwtrrVD  31561  snssiALTVD  31563  snsslVD  31565  snelpwrVD  31567  unipwrVD  31568  sstrALT2VD  31570  suctrALT2VD  31572  elex2VD  31574  elex22VD  31575  eqsbc3rVD  31576  zfregs2VD  31577  tpid3gVD  31578  en3lplem1VD  31579  en3lplem2VD  31580  en3lpVD  31581  3ornot23VD  31583  orbi1rVD  31584  3orbi123VD  31586  sbc3orgVD  31587  19.21a3con13vVD  31588  exbirVD  31589  exbiriVD  31590  rspsbc2VD  31591  3impexpVD  31592  3impexpbicomVD  31593  sbcoreleleqVD  31595  tratrbVD  31597  3ax4VD  31598  syl5impVD  31599  ssralv2VD  31602  ordelordALTVD  31603  equncomVD  31604  imbi12VD  31609  imbi13VD  31610  sbcim2gVD  31611  sbcbiVD  31612  trsbcVD  31613  truniALTVD  31614  trintALTVD  31616  undif3VD  31618  sbcssgVD  31619  csbingVD  31620  simplbi2comtVD  31624  onfrALTVD  31627  csbeq2gVD  31628  csbsngVD  31629  csbxpgVD  31630  csbresgVD  31631  csbrngVD  31632  csbima12gALTVD  31633  csbunigVD  31634  csbfv12gALTVD  31635  con5VD  31636  relopabVD  31637  19.41rgVD  31638  2pm13.193VD  31639  hbimpgVD  31640  hbalgVD  31641  hbexgVD  31642  ax6e2eqVD  31643  ax6e2ndVD  31644  ax6e2ndeqVD  31645  2sb5ndVD  31646  2uasbanhVD  31647  e2ebindVD  31648  sb5ALTVD  31649  vk15.4jVD  31650  notnot2ALTVD  31651  con3ALTVD  31652  sspwimpVD  31655  sspwimpcfVD  31657  suctrALTcfVD  31659
  Copyright terms: Public domain W3C validator