Theorem idn1 39744

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

Syntax hints:  (   wvd1 39739

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 199  df-vd1 39740

This theorem is referenced by:  trsspwALT  39997  sspwtr  40000  pwtrVD  40003  pwtrrVD  40004  snssiALTVD  40006  snsslVD  40008  snelpwrVD  40010  unipwrVD  40011  sstrALT2VD  40013  suctrALT2VD  40015  elex2VD  40017  elex22VD  40018  eqsbc3rVD  40019  zfregs2VD  40020  tpid3gVD  40021  en3lplem1VD  40022  en3lplem2VD  40023  en3lpVD  40024  3ornot23VD  40026  orbi1rVD  40027  3orbi123VD  40029  sbc3orgVD  40030  19.21a3con13vVD  40031  exbirVD  40032  exbiriVD  40033  rspsbc2VD  40034  3impexpVD  40035  3impexpbicomVD  40036  tratrbVD  40040  al2imVD  40041  syl5impVD  40042  ssralv2VD  40045  ordelordALTVD  40046  equncomVD  40047  imbi12VD  40052  imbi13VD  40053  sbcim2gVD  40054  sbcbiVD  40055  trsbcVD  40056  truniALTVD  40057  trintALTVD  40059  undif3VD  40061  sbcssgVD  40062  csbingVD  40063  onfrALTlem3VD  40066  simplbi2comtVD  40067  onfrALTlem2VD  40068  onfrALTVD  40070  csbeq2gVD  40071  csbsngVD  40072  csbxpgVD  40073  csbresgVD  40074  csbrngVD  40075  csbima12gALTVD  40076  csbunigVD  40077  csbfv12gALTVD  40078  con5VD  40079  relopabVD  40080  19.41rgVD  40081  2pm13.193VD  40082  hbimpgVD  40083  hbalgVD  40084  hbexgVD  40085  ax6e2eqVD  40086  ax6e2ndVD  40087  ax6e2ndeqVD  40088  2sb5ndVD  40089  2uasbanhVD  40090  e2ebindVD  40091  sb5ALTVD  40092  vk15.4jVD  40093  notnotrALTVD  40094  con3ALTVD  40095  sspwimpVD  40098  sspwimpcfVD  40100  suctrALTcfVD  40102