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

Theorem in1 28662
Description: Inference form of df-vd1 28661. 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 28661 . 2  |-  ( (.
ph 
->.  ps ).  <->  ( ph  ->  ps ) )
31, 2mpbi 200 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28660
This theorem is referenced by:  vd12  28701  vd13  28702  gen11nv  28718  gen12  28719  exinst11  28727  e1_  28728  el1  28729  e223  28736  e111  28775  e1111  28776  el2122old  28829  el12  28838  el123  28876  un0.1  28891  trsspwALT  28931  sspwtr  28934  pwtrVD  28937  pwtrrVD  28938  snssiALTVD  28939  snsslVD  28941  snelpwrVD  28943  unipwrVD  28944  sstrALT2VD  28946  suctrALT2VD  28948  elex2VD  28950  elex22VD  28951  eqsbc3rVD  28952  zfregs2VD  28953  tpid3gVD  28954  en3lplem1VD  28955  en3lplem2VD  28956  en3lpVD  28957  3ornot23VD  28959  orbi1rVD  28960  3orbi123VD  28962  sbc3orgVD  28963  19.21a3con13vVD  28964  exbirVD  28965  exbiriVD  28966  rspsbc2VD  28967  3impexpVD  28968  3impexpbicomVD  28969  sbcoreleleqVD  28971  tratrbVD  28973  3ax5VD  28974  syl5impVD  28975  ssralv2VD  28978  ordelordALTVD  28979  equncomVD  28980  imbi12VD  28985  imbi13VD  28986  sbcim2gVD  28987  sbcbiVD  28988  trsbcVD  28989  truniALTVD  28990  trintALTVD  28992  undif3VD  28994  sbcssVD  28995  csbingVD  28996  simplbi2comgVD  29000  onfrALTVD  29003  csbeq2gVD  29004  csbsngVD  29005  csbxpgVD  29006  csbresgVD  29007  csbrngVD  29008  csbima12gALTVD  29009  csbunigVD  29010  csbfv12gALTVD  29011  con5VD  29012  relopabVD  29013  19.41rgVD  29014  2pm13.193VD  29015  hbimpgVD  29016  hbalgVD  29017  hbexgVD  29018  a9e2eqVD  29019  a9e2ndVD  29020  a9e2ndeqVD  29021  2sb5ndVD  29022  2uasbanhVD  29023  e2ebindVD  29024  sb5ALTVD  29025  vk15.4jVD  29026  notnot2ALTVD  29027  con3ALTVD  29028  sspwimpVD  29031  sspwimpcfVD  29033  suctrALTcfVD  29035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-vd1 28661
  Copyright terms: Public domain W3C validator