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

Theorem idn1 31639
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 31638 1  |-  (. ph  ->.  ph ).
Colors of variables: wff setvar class
Syntax hints:   (.wvd1 31634
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 31635
This theorem is referenced by:  trsspwALT  31904  sspwtr  31907  pwtrVD  31912  pwtrrVD  31913  snssiALTVD  31915  snsslVD  31917  snelpwrVD  31919  unipwrVD  31920  sstrALT2VD  31922  suctrALT2VD  31924  elex2VD  31926  elex22VD  31927  eqsbc3rVD  31928  zfregs2VD  31929  tpid3gVD  31930  en3lplem1VD  31931  en3lplem2VD  31932  en3lpVD  31933  3ornot23VD  31935  orbi1rVD  31936  3orbi123VD  31938  sbc3orgVD  31939  19.21a3con13vVD  31940  exbirVD  31941  exbiriVD  31942  rspsbc2VD  31943  3impexpVD  31944  3impexpbicomVD  31945  sbcoreleleqVD  31947  tratrbVD  31949  3ax4VD  31950  syl5impVD  31951  ssralv2VD  31954  ordelordALTVD  31955  equncomVD  31956  imbi12VD  31961  imbi13VD  31962  sbcim2gVD  31963  sbcbiVD  31964  trsbcVD  31965  truniALTVD  31966  trintALTVD  31968  undif3VD  31970  sbcssgVD  31971  csbingVD  31972  onfrALTlem3VD  31975  simplbi2comtVD  31976  onfrALTlem2VD  31977  onfrALTVD  31979  csbeq2gVD  31980  csbsngVD  31981  csbxpgVD  31982  csbresgVD  31983  csbrngVD  31984  csbima12gALTVD  31985  csbunigVD  31986  csbfv12gALTVD  31987  con5VD  31988  relopabVD  31989  19.41rgVD  31990  2pm13.193VD  31991  hbimpgVD  31992  hbalgVD  31993  hbexgVD  31994  ax6e2eqVD  31995  ax6e2ndVD  31996  ax6e2ndeqVD  31997  2sb5ndVD  31998  2uasbanhVD  31999  e2ebindVD  32000  sb5ALTVD  32001  vk15.4jVD  32002  notnot2ALTVD  32003  con3ALTVD  32004  sspwimpVD  32007  sspwimpcfVD  32009  suctrALTcfVD  32011
  Copyright terms: Public domain W3C validator