Theorem idn1 40928

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

Syntax hints:  (   wvd1 40923

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 209  df-vd1 40924

This theorem is referenced by:  trsspwALT  41172  sspwtr  41175  pwtrVD  41178  pwtrrVD  41179  snssiALTVD  41181  snsslVD  41183  snelpwrVD  41185  unipwrVD  41186  sstrALT2VD  41188  suctrALT2VD  41190  elex2VD  41192  elex22VD  41193  eqsbc3rVD  41194  zfregs2VD  41195  tpid3gVD  41196  en3lplem1VD  41197  en3lplem2VD  41198  en3lpVD  41199  3ornot23VD  41201  orbi1rVD  41202  3orbi123VD  41204  sbc3orgVD  41205  19.21a3con13vVD  41206  exbirVD  41207  exbiriVD  41208  rspsbc2VD  41209  3impexpVD  41210  3impexpbicomVD  41211  tratrbVD  41215  al2imVD  41216  syl5impVD  41217  ssralv2VD  41220  ordelordALTVD  41221  equncomVD  41222  imbi12VD  41227  imbi13VD  41228  sbcim2gVD  41229  sbcbiVD  41230  trsbcVD  41231  truniALTVD  41232  trintALTVD  41234  undif3VD  41236  sbcssgVD  41237  csbingVD  41238  onfrALTlem3VD  41241  simplbi2comtVD  41242  onfrALTlem2VD  41243  onfrALTVD  41245  csbeq2gVD  41246  csbsngVD  41247  csbxpgVD  41248  csbresgVD  41249  csbrngVD  41250  csbima12gALTVD  41251  csbunigVD  41252  csbfv12gALTVD  41253  con5VD  41254  relopabVD  41255  19.41rgVD  41256  2pm13.193VD  41257  hbimpgVD  41258  hbalgVD  41259  hbexgVD  41260  ax6e2eqVD  41261  ax6e2ndVD  41262  ax6e2ndeqVD  41263  2sb5ndVD  41264  2uasbanhVD  41265  e2ebindVD  41266  sb5ALTVD  41267  vk15.4jVD  41268  notnotrALTVD  41269  con3ALTVD  41270  sspwimpVD  41273  sspwimpcfVD  41275  suctrALTcfVD  41277