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

Theorem in1 33761
Description: Inference form of df-vd1 33760. 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 33760 . 2  |-  ( (.
ph 
->.  ps ).  <->  ( ph  ->  ps ) )
31, 2mpbi 208 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 33759
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 33760
This theorem is referenced by:  vd12  33799  vd13  33800  gen11nv  33816  gen12  33817  exinst11  33825  e1a  33826  el1  33827  e223  33834  e111  33873  e1111  33874  el2122old  33927  el12  33936  el123  33974  un0.1  33989  trsspwALT  34029  sspwtr  34032  pwtrVD  34043  pwtrrVD  34044  snssiALTVD  34046  snsslVD  34048  snelpwrVD  34050  unipwrVD  34051  sstrALT2VD  34053  suctrALT2VD  34055  elex2VD  34057  elex22VD  34058  eqsbc3rVD  34059  zfregs2VD  34060  tpid3gVD  34061  en3lplem1VD  34062  en3lplem2VD  34063  en3lpVD  34064  3ornot23VD  34066  orbi1rVD  34067  3orbi123VD  34069  sbc3orgVD  34070  19.21a3con13vVD  34071  exbirVD  34072  exbiriVD  34073  rspsbc2VD  34074  3impexpVD  34075  3impexpbicomVD  34076  sbcoreleleqVD  34079  tratrbVD  34081  al2imVD  34082  syl5impVD  34083  ssralv2VD  34086  ordelordALTVD  34087  equncomVD  34088  imbi12VD  34093  imbi13VD  34094  sbcim2gVD  34095  sbcbiVD  34096  trsbcVD  34097  truniALTVD  34098  trintALTVD  34100  undif3VD  34102  sbcssgVD  34103  csbingVD  34104  simplbi2comtVD  34108  onfrALTVD  34111  csbeq2gVD  34112  csbsngVD  34113  csbxpgVD  34114  csbresgVD  34115  csbrngVD  34116  csbima12gALTVD  34117  csbunigVD  34118  csbfv12gALTVD  34119  con5VD  34120  relopabVD  34121  19.41rgVD  34122  2pm13.193VD  34123  hbimpgVD  34124  hbalgVD  34125  hbexgVD  34126  ax6e2eqVD  34127  ax6e2ndVD  34128  ax6e2ndeqVD  34129  2sb5ndVD  34130  2uasbanhVD  34131  e2ebindVD  34132  sb5ALTVD  34133  vk15.4jVD  34134  notnot2ALTVD  34135  con3ALTVD  34136  sspwimpVD  34139  sspwimpcfVD  34141  suctrALTcfVD  34143
  Copyright terms: Public domain W3C validator