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

Theorem idn1 36916
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 36915 1  |-  (. ph  ->.  ph ).
Colors of variables: wff setvar class
Syntax hints:   (.wvd1 36911
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 36912
This theorem is referenced by:  trsspwALT  37180  sspwtr  37183  pwtrVD  37194  pwtrrVD  37195  snssiALTVD  37197  snsslVD  37199  snelpwrVD  37201  unipwrVD  37202  sstrALT2VD  37204  suctrALT2VD  37206  elex2VD  37208  elex22VD  37209  eqsbc3rVD  37210  zfregs2VD  37211  tpid3gVD  37212  en3lplem1VD  37213  en3lplem2VD  37214  en3lpVD  37215  3ornot23VD  37217  orbi1rVD  37218  3orbi123VD  37220  sbc3orgVD  37221  19.21a3con13vVD  37222  exbirVD  37223  exbiriVD  37224  rspsbc2VD  37225  3impexpVD  37226  3impexpbicomVD  37227  sbcoreleleqVD  37230  tratrbVD  37232  al2imVD  37233  syl5impVD  37234  ssralv2VD  37237  ordelordALTVD  37238  equncomVD  37239  imbi12VD  37244  imbi13VD  37245  sbcim2gVD  37246  sbcbiVD  37247  trsbcVD  37248  truniALTVD  37249  trintALTVD  37251  undif3VD  37253  sbcssgVD  37254  csbingVD  37255  onfrALTlem3VD  37258  simplbi2comtVD  37259  onfrALTlem2VD  37260  onfrALTVD  37262  csbeq2gVD  37263  csbsngVD  37264  csbxpgVD  37265  csbresgVD  37266  csbrngVD  37267  csbima12gALTVD  37268  csbunigVD  37269  csbfv12gALTVD  37270  con5VD  37271  relopabVD  37272  19.41rgVD  37273  2pm13.193VD  37274  hbimpgVD  37275  hbalgVD  37276  hbexgVD  37277  ax6e2eqVD  37278  ax6e2ndVD  37279  ax6e2ndeqVD  37280  2sb5ndVD  37281  2uasbanhVD  37282  e2ebindVD  37283  sb5ALTVD  37284  vk15.4jVD  37285  notnot2ALTVD  37286  con3ALTVD  37287  sspwimpVD  37290  sspwimpcfVD  37292  suctrALTcfVD  37294
  Copyright terms: Public domain W3C validator