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

Theorem in1 36855
Description: Inference form of df-vd1 36854. 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 36854 . 2  |-  ( (.
ph 
->.  ps ).  <->  ( ph  ->  ps ) )
31, 2mpbi 211 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 36853
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 188  df-vd1 36854
This theorem is referenced by:  vd12  36893  vd13  36894  gen11nv  36910  gen12  36911  exinst11  36919  e1a  36920  el1  36921  e223  36928  e111  36967  e1111  36968  el2122old  37020  el12  37029  el123  37067  un0.1  37082  trsspwALT  37122  sspwtr  37125  pwtrVD  37136  pwtrrVD  37137  snssiALTVD  37139  snsslVD  37141  snelpwrVD  37143  unipwrVD  37144  sstrALT2VD  37146  suctrALT2VD  37148  elex2VD  37150  elex22VD  37151  eqsbc3rVD  37152  zfregs2VD  37153  tpid3gVD  37154  en3lplem1VD  37155  en3lplem2VD  37156  en3lpVD  37157  3ornot23VD  37159  orbi1rVD  37160  3orbi123VD  37162  sbc3orgVD  37163  19.21a3con13vVD  37164  exbirVD  37165  exbiriVD  37166  rspsbc2VD  37167  3impexpVD  37168  3impexpbicomVD  37169  sbcoreleleqVD  37172  tratrbVD  37174  al2imVD  37175  syl5impVD  37176  ssralv2VD  37179  ordelordALTVD  37180  equncomVD  37181  imbi12VD  37186  imbi13VD  37187  sbcim2gVD  37188  sbcbiVD  37189  trsbcVD  37190  truniALTVD  37191  trintALTVD  37193  undif3VD  37195  sbcssgVD  37196  csbingVD  37197  simplbi2comtVD  37201  onfrALTVD  37204  csbeq2gVD  37205  csbsngVD  37206  csbxpgVD  37207  csbresgVD  37208  csbrngVD  37209  csbima12gALTVD  37210  csbunigVD  37211  csbfv12gALTVD  37212  con5VD  37213  relopabVD  37214  19.41rgVD  37215  2pm13.193VD  37216  hbimpgVD  37217  hbalgVD  37218  hbexgVD  37219  ax6e2eqVD  37220  ax6e2ndVD  37221  ax6e2ndeqVD  37222  2sb5ndVD  37223  2uasbanhVD  37224  e2ebindVD  37225  sb5ALTVD  37226  vk15.4jVD  37227  notnot2ALTVD  37228  con3ALTVD  37229  sspwimpVD  37232  sspwimpcfVD  37234  suctrALTcfVD  37236
  Copyright terms: Public domain W3C validator