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

Theorem in1 31025
Description: Inference form of df-vd1 31024. 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 31024 . 2  |-  ( (.
ph 
->.  ps ).  <->  ( ph  ->  ps ) )
31, 2mpbi 208 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 31023
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 31024
This theorem is referenced by:  vd12  31064  vd13  31065  gen11nv  31081  gen12  31082  exinst11  31090  e1_  31091  el1  31092  e223  31099  e111  31138  e1111  31139  el2122old  31192  el12  31201  el123  31239  un0.1  31254  trsspwALT  31294  sspwtr  31297  pwtrVD  31302  pwtrrVD  31303  snssiALTVD  31305  snsslVD  31307  snelpwrVD  31309  unipwrVD  31310  sstrALT2VD  31312  suctrALT2VD  31314  elex2VD  31316  elex22VD  31317  eqsbc3rVD  31318  zfregs2VD  31319  tpid3gVD  31320  en3lplem1VD  31321  en3lplem2VD  31322  en3lpVD  31323  3ornot23VD  31325  orbi1rVD  31326  3orbi123VD  31328  sbc3orgVD  31329  19.21a3con13vVD  31330  exbirVD  31331  exbiriVD  31332  rspsbc2VD  31333  3impexpVD  31334  3impexpbicomVD  31335  sbcoreleleqVD  31337  tratrbVD  31339  3ax4VD  31340  syl5impVD  31341  ssralv2VD  31344  ordelordALTVD  31345  equncomVD  31346  imbi12VD  31351  imbi13VD  31352  sbcim2gVD  31353  sbcbiVD  31354  trsbcVD  31355  truniALTVD  31356  trintALTVD  31358  undif3VD  31360  sbcssgVD  31361  csbingVD  31362  simplbi2comgVD  31366  onfrALTVD  31369  csbeq2gVD  31370  csbsngVD  31371  csbxpgVD  31372  csbresgVD  31373  csbrngVD  31374  csbima12gALTVD  31375  csbunigVD  31376  csbfv12gALTVD  31377  con5VD  31378  relopabVD  31379  19.41rgVD  31380  2pm13.193VD  31381  hbimpgVD  31382  hbalgVD  31383  hbexgVD  31384  ax6e2eqVD  31385  ax6e2ndVD  31386  ax6e2ndeqVD  31387  2sb5ndVD  31388  2uasbanhVD  31389  e2ebindVD  31390  sb5ALTVD  31391  vk15.4jVD  31392  notnot2ALTVD  31393  con3ALTVD  31394  sspwimpVD  31397  sspwimpcfVD  31399  suctrALTcfVD  31401
  Copyright terms: Public domain W3C validator