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

Theorem in1 28339
Description: Inference form of df-vd1 28338. 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 28338 . 2  |-  ( (.
ph 
->.  ps ).  <->  ( ph  ->  ps ) )
31, 2mpbi 199 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   (.wvd1 28337
This theorem is referenced by:  vd12  28372  vd13  28373  gen11nv  28389  gen12  28390  exinst11  28398  e1_  28399  el1  28400  e223  28407  e111  28446  e1111  28447  el2122old  28498  el12  28501  el123  28539  un0.1  28554  trsspwALT  28592  sspwtr  28595  pwtrVD  28598  pwtrrVD  28600  snssiALTVD  28602  snsslVD  28604  snelpwrVD  28606  unipwrVD  28608  sstrALT2VD  28610  suctrALT2VD  28612  elex2VD  28614  elex22VD  28615  eqsbc3rVD  28616  zfregs2VD  28617  tpid3gVD  28618  en3lplem1VD  28619  en3lplem2VD  28620  en3lpVD  28621  3ornot23VD  28623  orbi1rVD  28624  3orbi123VD  28626  sbc3orgVD  28627  19.21a3con13vVD  28628  exbirVD  28629  exbiriVD  28630  rspsbc2VD  28631  3impexpVD  28632  3impexpbicomVD  28633  sbcoreleleqVD  28635  tratrbVD  28637  3ax5VD  28638  syl5impVD  28639  ssralv2VD  28642  ordelordALTVD  28643  equncomVD  28644  imbi12VD  28649  imbi13VD  28650  sbcim2gVD  28651  sbcbiVD  28652  trsbcVD  28653  truniALTVD  28654  trintALTVD  28656  undif3VD  28658  sbcssVD  28659  csbingVD  28660  simplbi2comgVD  28664  onfrALTVD  28667  csbeq2gVD  28668  csbsngVD  28669  csbxpgVD  28670  csbresgVD  28671  csbrngVD  28672  csbima12gALTVD  28673  csbunigVD  28674  csbfv12gALTVD  28675  con5VD  28676  relopabVD  28677  19.41rgVD  28678  2pm13.193VD  28679  hbimpgVD  28680  hbalgVD  28681  hbexgVD  28682  a9e2eqVD  28683  a9e2ndVD  28684  a9e2ndeqVD  28685  2sb5ndVD  28686  2uasbanhVD  28687  e2ebindVD  28688  sb5ALTVD  28689  vk15.4jVD  28690  notnot2ALTVD  28691  con3ALTVD  28692  sspwimpVD  28695  sspwimpcfVD  28697  suctrALTcfVD  28699
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 177  df-vd1 28338
  Copyright terms: Public domain W3C validator