Theorem idn1 45004

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

Syntax hints:  (   wvd1 44999

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 45000

This theorem is referenced by:  trsspwALT  45247  sspwtr  45250  pwtrVD  45253  pwtrrVD  45254  snssiALTVD  45256  snsslVD  45258  snelpwrVD  45260  unipwrVD  45261  sstrALT2VD  45263  suctrALT2VD  45265  elex2VD  45267  elex22VD  45268  eqsbc2VD  45269  zfregs2VD  45270  tpid3gVD  45271  en3lplem1VD  45272  en3lplem2VD  45273  en3lpVD  45274  3ornot23VD  45276  orbi1rVD  45277  3orbi123VD  45279  sbc3orgVD  45280  19.21a3con13vVD  45281  exbirVD  45282  exbiriVD  45283  rspsbc2VD  45284  3impexpVD  45285  3impexpbicomVD  45286  tratrbVD  45290  al2imVD  45291  syl5impVD  45292  ssralv2VD  45295  ordelordALTVD  45296  equncomVD  45297  imbi12VD  45302  imbi13VD  45303  sbcim2gVD  45304  sbcbiVD  45305  trsbcVD  45306  truniALTVD  45307  trintALTVD  45309  undif3VD  45311  sbcssgVD  45312  csbingVD  45313  onfrALTlem3VD  45316  simplbi2comtVD  45317  onfrALTlem2VD  45318  onfrALTVD  45320  csbeq2gVD  45321  csbsngVD  45322  csbxpgVD  45323  csbresgVD  45324  csbrngVD  45325  csbima12gALTVD  45326  csbunigVD  45327  csbfv12gALTVD  45328  con5VD  45329  relopabVD  45330  19.41rgVD  45331  2pm13.193VD  45332  hbimpgVD  45333  hbalgVD  45334  hbexgVD  45335  ax6e2eqVD  45336  ax6e2ndVD  45337  ax6e2ndeqVD  45338  2sb5ndVD  45339  2uasbanhVD  45340  e2ebindVD  45341  sb5ALTVD  45342  vk15.4jVD  45343  notnotrALTVD  45344  con3ALTVD  45345  sspwimpVD  45348  sspwimpcfVD  45350  suctrALTcfVD  45352