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

Theorem idn1 32440
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 32439 1  |-  (. ph  ->.  ph ).
Colors of variables: wff setvar class
Syntax hints:   (.wvd1 32435
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 32436
This theorem is referenced by:  trsspwALT  32705  sspwtr  32708  pwtrVD  32713  pwtrrVD  32714  snssiALTVD  32716  snsslVD  32718  snelpwrVD  32720  unipwrVD  32721  sstrALT2VD  32723  suctrALT2VD  32725  elex2VD  32727  elex22VD  32728  eqsbc3rVD  32729  zfregs2VD  32730  tpid3gVD  32731  en3lplem1VD  32732  en3lplem2VD  32733  en3lpVD  32734  3ornot23VD  32736  orbi1rVD  32737  3orbi123VD  32739  sbc3orgVD  32740  19.21a3con13vVD  32741  exbirVD  32742  exbiriVD  32743  rspsbc2VD  32744  3impexpVD  32745  3impexpbicomVD  32746  sbcoreleleqVD  32748  tratrbVD  32750  3ax4VD  32751  syl5impVD  32752  ssralv2VD  32755  ordelordALTVD  32756  equncomVD  32757  imbi12VD  32762  imbi13VD  32763  sbcim2gVD  32764  sbcbiVD  32765  trsbcVD  32766  truniALTVD  32767  trintALTVD  32769  undif3VD  32771  sbcssgVD  32772  csbingVD  32773  onfrALTlem3VD  32776  simplbi2comtVD  32777  onfrALTlem2VD  32778  onfrALTVD  32780  csbeq2gVD  32781  csbsngVD  32782  csbxpgVD  32783  csbresgVD  32784  csbrngVD  32785  csbima12gALTVD  32786  csbunigVD  32787  csbfv12gALTVD  32788  con5VD  32789  relopabVD  32790  19.41rgVD  32791  2pm13.193VD  32792  hbimpgVD  32793  hbalgVD  32794  hbexgVD  32795  ax6e2eqVD  32796  ax6e2ndVD  32797  ax6e2ndeqVD  32798  2sb5ndVD  32799  2uasbanhVD  32800  e2ebindVD  32801  sb5ALTVD  32802  vk15.4jVD  32803  notnot2ALTVD  32804  con3ALTVD  32805  sspwimpVD  32808  sspwimpcfVD  32810  suctrALTcfVD  32812
  Copyright terms: Public domain W3C validator