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

Theorem idn1 33452
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 33451 1  |-  (. ph  ->.  ph ).
Colors of variables: wff setvar class
Syntax hints:   (.wvd1 33447
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 33448
This theorem is referenced by:  trsspwALT  33717  sspwtr  33720  pwtrVD  33725  pwtrrVD  33726  snssiALTVD  33728  snsslVD  33730  snelpwrVD  33732  unipwrVD  33733  sstrALT2VD  33735  suctrALT2VD  33737  elex2VD  33739  elex22VD  33740  eqsbc3rVD  33741  zfregs2VD  33742  tpid3gVD  33743  en3lplem1VD  33744  en3lplem2VD  33745  en3lpVD  33746  3ornot23VD  33748  orbi1rVD  33749  3orbi123VD  33751  sbc3orgVD  33752  19.21a3con13vVD  33753  exbirVD  33754  exbiriVD  33755  rspsbc2VD  33756  3impexpVD  33757  3impexpbicomVD  33758  sbcoreleleqVD  33760  tratrbVD  33762  al2imVD  33763  syl5impVD  33764  ssralv2VD  33767  ordelordALTVD  33768  equncomVD  33769  imbi12VD  33774  imbi13VD  33775  sbcim2gVD  33776  sbcbiVD  33777  trsbcVD  33778  truniALTVD  33779  trintALTVD  33781  undif3VD  33783  sbcssgVD  33784  csbingVD  33785  onfrALTlem3VD  33788  simplbi2comtVD  33789  onfrALTlem2VD  33790  onfrALTVD  33792  csbeq2gVD  33793  csbsngVD  33794  csbxpgVD  33795  csbresgVD  33796  csbrngVD  33797  csbima12gALTVD  33798  csbunigVD  33799  csbfv12gALTVD  33800  con5VD  33801  relopabVD  33802  19.41rgVD  33803  2pm13.193VD  33804  hbimpgVD  33805  hbalgVD  33806  hbexgVD  33807  ax6e2eqVD  33808  ax6e2ndVD  33809  ax6e2ndeqVD  33810  2sb5ndVD  33811  2uasbanhVD  33812  e2ebindVD  33813  sb5ALTVD  33814  vk15.4jVD  33815  notnot2ALTVD  33816  con3ALTVD  33817  sspwimpVD  33820  sspwimpcfVD  33822  suctrALTcfVD  33824
  Copyright terms: Public domain W3C validator