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

Theorem idn1 36944
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 36943 1  |-  (. ph  ->.  ph ).
Colors of variables: wff setvar class
Syntax hints:   (.wvd1 36939
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 190  df-vd1 36940
This theorem is referenced by:  trsspwALT  37203  sspwtr  37206  pwtrVD  37217  pwtrrVD  37218  snssiALTVD  37220  snsslVD  37222  snelpwrVD  37224  unipwrVD  37225  sstrALT2VD  37227  suctrALT2VD  37229  elex2VD  37231  elex22VD  37232  eqsbc3rVD  37233  zfregs2VD  37234  tpid3gVD  37235  en3lplem1VD  37236  en3lplem2VD  37237  en3lpVD  37238  3ornot23VD  37240  orbi1rVD  37241  3orbi123VD  37243  sbc3orgVD  37244  19.21a3con13vVD  37245  exbirVD  37246  exbiriVD  37247  rspsbc2VD  37248  3impexpVD  37249  3impexpbicomVD  37250  sbcoreleleqVD  37253  tratrbVD  37255  al2imVD  37256  syl5impVD  37257  ssralv2VD  37260  ordelordALTVD  37261  equncomVD  37262  imbi12VD  37267  imbi13VD  37268  sbcim2gVD  37269  sbcbiVD  37270  trsbcVD  37271  truniALTVD  37272  trintALTVD  37274  undif3VD  37276  sbcssgVD  37277  csbingVD  37278  onfrALTlem3VD  37281  simplbi2comtVD  37282  onfrALTlem2VD  37283  onfrALTVD  37285  csbeq2gVD  37286  csbsngVD  37287  csbxpgVD  37288  csbresgVD  37289  csbrngVD  37290  csbima12gALTVD  37291  csbunigVD  37292  csbfv12gALTVD  37293  con5VD  37294  relopabVD  37295  19.41rgVD  37296  2pm13.193VD  37297  hbimpgVD  37298  hbalgVD  37299  hbexgVD  37300  ax6e2eqVD  37301  ax6e2ndVD  37302  ax6e2ndeqVD  37303  2sb5ndVD  37304  2uasbanhVD  37305  e2ebindVD  37306  sb5ALTVD  37307  vk15.4jVD  37308  notnot2ALTVD  37309  con3ALTVD  37310  sspwimpVD  37313  sspwimpcfVD  37315  suctrALTcfVD  37317
  Copyright terms: Public domain W3C validator