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

Theorem idn1 31174
Description: Virtual deduction identity rule which is id 22 with virtual deduction symbols. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
idn1  |-  (. ph  ->.  ph ).

Proof of Theorem idn1
StepHypRef Expression
1 id 22 . 2  |-  ( ph  ->  ph )
21dfvd1ir 31173 1  |-  (. ph  ->.  ph ).
Colors of variables: wff setvar class
Syntax hints:   (.wvd1 31169
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 31170
This theorem is referenced by:  trsspwALT  31439  sspwtr  31442  pwtrVD  31447  pwtrrVD  31448  snssiALTVD  31450  snsslVD  31452  snelpwrVD  31454  unipwrVD  31455  sstrALT2VD  31457  suctrALT2VD  31459  elex2VD  31461  elex22VD  31462  eqsbc3rVD  31463  zfregs2VD  31464  tpid3gVD  31465  en3lplem1VD  31466  en3lplem2VD  31467  en3lpVD  31468  3ornot23VD  31470  orbi1rVD  31471  3orbi123VD  31473  sbc3orgVD  31474  19.21a3con13vVD  31475  exbirVD  31476  exbiriVD  31477  rspsbc2VD  31478  3impexpVD  31479  3impexpbicomVD  31480  sbcoreleleqVD  31482  tratrbVD  31484  3ax4VD  31485  syl5impVD  31486  ssralv2VD  31489  ordelordALTVD  31490  equncomVD  31491  imbi12VD  31496  imbi13VD  31497  sbcim2gVD  31498  sbcbiVD  31499  trsbcVD  31500  truniALTVD  31501  trintALTVD  31503  undif3VD  31505  sbcssgVD  31506  csbingVD  31507  onfrALTlem3VD  31510  simplbi2comtVD  31511  onfrALTlem2VD  31512  onfrALTVD  31514  csbeq2gVD  31515  csbsngVD  31516  csbxpgVD  31517  csbresgVD  31518  csbrngVD  31519  csbima12gALTVD  31520  csbunigVD  31521  csbfv12gALTVD  31522  con5VD  31523  relopabVD  31524  19.41rgVD  31525  2pm13.193VD  31526  hbimpgVD  31527  hbalgVD  31528  hbexgVD  31529  ax6e2eqVD  31530  ax6e2ndVD  31531  ax6e2ndeqVD  31532  2sb5ndVD  31533  2uasbanhVD  31534  e2ebindVD  31535  sb5ALTVD  31536  vk15.4jVD  31537  notnot2ALTVD  31538  con3ALTVD  31539  sspwimpVD  31542  sspwimpcfVD  31544  suctrALTcfVD  31546
  Copyright terms: Public domain W3C validator