Theorem idn1 41280

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	⊢ (   𝜑   ▶   𝜑   )

Proof of Theorem idn1

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2	1	dfvd1ir 41279	1 ⊢ (   𝜑   ▶   𝜑   )

Syntax hints:  (   wvd1 41275

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 210  df-vd1 41276

This theorem is referenced by:  trsspwALT  41524  sspwtr  41527  pwtrVD  41530  pwtrrVD  41531  snssiALTVD  41533  snsslVD  41535  snelpwrVD  41537  unipwrVD  41538  sstrALT2VD  41540  suctrALT2VD  41542  elex2VD  41544  elex22VD  41545  eqsbc3rVD  41546  zfregs2VD  41547  tpid3gVD  41548  en3lplem1VD  41549  en3lplem2VD  41550  en3lpVD  41551  3ornot23VD  41553  orbi1rVD  41554  3orbi123VD  41556  sbc3orgVD  41557  19.21a3con13vVD  41558  exbirVD  41559  exbiriVD  41560  rspsbc2VD  41561  3impexpVD  41562  3impexpbicomVD  41563  tratrbVD  41567  al2imVD  41568  syl5impVD  41569  ssralv2VD  41572  ordelordALTVD  41573  equncomVD  41574  imbi12VD  41579  imbi13VD  41580  sbcim2gVD  41581  sbcbiVD  41582  trsbcVD  41583  truniALTVD  41584  trintALTVD  41586  undif3VD  41588  sbcssgVD  41589  csbingVD  41590  onfrALTlem3VD  41593  simplbi2comtVD  41594  onfrALTlem2VD  41595  onfrALTVD  41597  csbeq2gVD  41598  csbsngVD  41599  csbxpgVD  41600  csbresgVD  41601  csbrngVD  41602  csbima12gALTVD  41603  csbunigVD  41604  csbfv12gALTVD  41605  con5VD  41606  relopabVD  41607  19.41rgVD  41608  2pm13.193VD  41609  hbimpgVD  41610  hbalgVD  41611  hbexgVD  41612  ax6e2eqVD  41613  ax6e2ndVD  41614  ax6e2ndeqVD  41615  2sb5ndVD  41616  2uasbanhVD  41617  e2ebindVD  41618  sb5ALTVD  41619  vk15.4jVD  41620  notnotrALTVD  41621  con3ALTVD  41622  sspwimpVD  41625  sspwimpcfVD  41627  suctrALTcfVD  41629