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

Theorem in1 32446
Description: Inference form of df-vd1 32445. 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 32445 . 2  |-  ( (.
ph 
->.  ps ).  <->  ( ph  ->  ps ) )
31, 2mpbi 208 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   (.wvd1 32444
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 32445
This theorem is referenced by:  vd12  32484  vd13  32485  gen11nv  32501  gen12  32502  exinst11  32510  e1a  32511  el1  32512  e223  32519  e111  32558  e1111  32559  el2122old  32612  el12  32621  el123  32659  un0.1  32674  trsspwALT  32714  sspwtr  32717  pwtrVD  32722  pwtrrVD  32723  snssiALTVD  32725  snsslVD  32727  snelpwrVD  32729  unipwrVD  32730  sstrALT2VD  32732  suctrALT2VD  32734  elex2VD  32736  elex22VD  32737  eqsbc3rVD  32738  zfregs2VD  32739  tpid3gVD  32740  en3lplem1VD  32741  en3lplem2VD  32742  en3lpVD  32743  3ornot23VD  32745  orbi1rVD  32746  3orbi123VD  32748  sbc3orgVD  32749  19.21a3con13vVD  32750  exbirVD  32751  exbiriVD  32752  rspsbc2VD  32753  3impexpVD  32754  3impexpbicomVD  32755  sbcoreleleqVD  32757  tratrbVD  32759  3ax4VD  32760  syl5impVD  32761  ssralv2VD  32764  ordelordALTVD  32765  equncomVD  32766  imbi12VD  32771  imbi13VD  32772  sbcim2gVD  32773  sbcbiVD  32774  trsbcVD  32775  truniALTVD  32776  trintALTVD  32778  undif3VD  32780  sbcssgVD  32781  csbingVD  32782  simplbi2comtVD  32786  onfrALTVD  32789  csbeq2gVD  32790  csbsngVD  32791  csbxpgVD  32792  csbresgVD  32793  csbrngVD  32794  csbima12gALTVD  32795  csbunigVD  32796  csbfv12gALTVD  32797  con5VD  32798  relopabVD  32799  19.41rgVD  32800  2pm13.193VD  32801  hbimpgVD  32802  hbalgVD  32803  hbexgVD  32804  ax6e2eqVD  32805  ax6e2ndVD  32806  ax6e2ndeqVD  32807  2sb5ndVD  32808  2uasbanhVD  32809  e2ebindVD  32810  sb5ALTVD  32811  vk15.4jVD  32812  notnot2ALTVD  32813  con3ALTVD  32814  sspwimpVD  32817  sspwimpcfVD  32819  suctrALTcfVD  32821
  Copyright terms: Public domain W3C validator