Theorem idn1 44545

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

Syntax hints:  (   wvd1 44540

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 207  df-vd1 44541

This theorem is referenced by:  trsspwALT  44789  sspwtr  44792  pwtrVD  44795  pwtrrVD  44796  snssiALTVD  44798  snsslVD  44800  snelpwrVD  44802  unipwrVD  44803  sstrALT2VD  44805  suctrALT2VD  44807  elex2VD  44809  elex22VD  44810  eqsbc2VD  44811  zfregs2VD  44812  tpid3gVD  44813  en3lplem1VD  44814  en3lplem2VD  44815  en3lpVD  44816  3ornot23VD  44818  orbi1rVD  44819  3orbi123VD  44821  sbc3orgVD  44822  19.21a3con13vVD  44823  exbirVD  44824  exbiriVD  44825  rspsbc2VD  44826  3impexpVD  44827  3impexpbicomVD  44828  tratrbVD  44832  al2imVD  44833  syl5impVD  44834  ssralv2VD  44837  ordelordALTVD  44838  equncomVD  44839  imbi12VD  44844  imbi13VD  44845  sbcim2gVD  44846  sbcbiVD  44847  trsbcVD  44848  truniALTVD  44849  trintALTVD  44851  undif3VD  44853  sbcssgVD  44854  csbingVD  44855  onfrALTlem3VD  44858  simplbi2comtVD  44859  onfrALTlem2VD  44860  onfrALTVD  44862  csbeq2gVD  44863  csbsngVD  44864  csbxpgVD  44865  csbresgVD  44866  csbrngVD  44867  csbima12gALTVD  44868  csbunigVD  44869  csbfv12gALTVD  44870  con5VD  44871  relopabVD  44872  19.41rgVD  44873  2pm13.193VD  44874  hbimpgVD  44875  hbalgVD  44876  hbexgVD  44877  ax6e2eqVD  44878  ax6e2ndVD  44879  ax6e2ndeqVD  44880  2sb5ndVD  44881  2uasbanhVD  44882  e2ebindVD  44883  sb5ALTVD  44884  vk15.4jVD  44885  notnotrALTVD  44886  con3ALTVD  44887  sspwimpVD  44890  sspwimpcfVD  44892  suctrALTcfVD  44894