Theorem idn1 44989

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

Syntax hints:  (   wvd1 44984

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 44985

This theorem is referenced by:  trsspwALT  45232  sspwtr  45235  pwtrVD  45238  pwtrrVD  45239  snssiALTVD  45241  snsslVD  45243  snelpwrVD  45245  unipwrVD  45246  sstrALT2VD  45248  suctrALT2VD  45250  elex2VD  45252  elex22VD  45253  eqsbc2VD  45254  zfregs2VD  45255  tpid3gVD  45256  en3lplem1VD  45257  en3lplem2VD  45258  en3lpVD  45259  3ornot23VD  45261  orbi1rVD  45262  3orbi123VD  45264  sbc3orgVD  45265  19.21a3con13vVD  45266  exbirVD  45267  exbiriVD  45268  rspsbc2VD  45269  3impexpVD  45270  3impexpbicomVD  45271  tratrbVD  45275  al2imVD  45276  syl5impVD  45277  ssralv2VD  45280  ordelordALTVD  45281  equncomVD  45282  imbi12VD  45287  imbi13VD  45288  sbcim2gVD  45289  sbcbiVD  45290  trsbcVD  45291  truniALTVD  45292  trintALTVD  45294  undif3VD  45296  sbcssgVD  45297  csbingVD  45298  onfrALTlem3VD  45301  simplbi2comtVD  45302  onfrALTlem2VD  45303  onfrALTVD  45305  csbeq2gVD  45306  csbsngVD  45307  csbxpgVD  45308  csbresgVD  45309  csbrngVD  45310  csbima12gALTVD  45311  csbunigVD  45312  csbfv12gALTVD  45313  con5VD  45314  relopabVD  45315  19.41rgVD  45316  2pm13.193VD  45317  hbimpgVD  45318  hbalgVD  45319  hbexgVD  45320  ax6e2eqVD  45321  ax6e2ndVD  45322  ax6e2ndeqVD  45323  2sb5ndVD  45324  2uasbanhVD  45325  e2ebindVD  45326  sb5ALTVD  45327  vk15.4jVD  45328  notnotrALTVD  45329  con3ALTVD  45330  sspwimpVD  45333  sspwimpcfVD  45335  suctrALTcfVD  45337