Theorem idn1 44557

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

Syntax hints:  (   wvd1 44552

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 44553

This theorem is referenced by:  trsspwALT  44800  sspwtr  44803  pwtrVD  44806  pwtrrVD  44807  snssiALTVD  44809  snsslVD  44811  snelpwrVD  44813  unipwrVD  44814  sstrALT2VD  44816  suctrALT2VD  44818  elex2VD  44820  elex22VD  44821  eqsbc2VD  44822  zfregs2VD  44823  tpid3gVD  44824  en3lplem1VD  44825  en3lplem2VD  44826  en3lpVD  44827  3ornot23VD  44829  orbi1rVD  44830  3orbi123VD  44832  sbc3orgVD  44833  19.21a3con13vVD  44834  exbirVD  44835  exbiriVD  44836  rspsbc2VD  44837  3impexpVD  44838  3impexpbicomVD  44839  tratrbVD  44843  al2imVD  44844  syl5impVD  44845  ssralv2VD  44848  ordelordALTVD  44849  equncomVD  44850  imbi12VD  44855  imbi13VD  44856  sbcim2gVD  44857  sbcbiVD  44858  trsbcVD  44859  truniALTVD  44860  trintALTVD  44862  undif3VD  44864  sbcssgVD  44865  csbingVD  44866  onfrALTlem3VD  44869  simplbi2comtVD  44870  onfrALTlem2VD  44871  onfrALTVD  44873  csbeq2gVD  44874  csbsngVD  44875  csbxpgVD  44876  csbresgVD  44877  csbrngVD  44878  csbima12gALTVD  44879  csbunigVD  44880  csbfv12gALTVD  44881  con5VD  44882  relopabVD  44883  19.41rgVD  44884  2pm13.193VD  44885  hbimpgVD  44886  hbalgVD  44887  hbexgVD  44888  ax6e2eqVD  44889  ax6e2ndVD  44890  ax6e2ndeqVD  44891  2sb5ndVD  44892  2uasbanhVD  44893  e2ebindVD  44894  sb5ALTVD  44895  vk15.4jVD  44896  notnotrALTVD  44897  con3ALTVD  44898  sspwimpVD  44901  sspwimpcfVD  44903  suctrALTcfVD  44905