Theorem idn1 42978

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

Syntax hints:  (   wvd1 42973

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 206  df-vd1 42974

This theorem is referenced by:  trsspwALT  43222  sspwtr  43225  pwtrVD  43228  pwtrrVD  43229  snssiALTVD  43231  snsslVD  43233  snelpwrVD  43235  unipwrVD  43236  sstrALT2VD  43238  suctrALT2VD  43240  elex2VD  43242  elex22VD  43243  eqsbc2VD  43244  zfregs2VD  43245  tpid3gVD  43246  en3lplem1VD  43247  en3lplem2VD  43248  en3lpVD  43249  3ornot23VD  43251  orbi1rVD  43252  3orbi123VD  43254  sbc3orgVD  43255  19.21a3con13vVD  43256  exbirVD  43257  exbiriVD  43258  rspsbc2VD  43259  3impexpVD  43260  3impexpbicomVD  43261  tratrbVD  43265  al2imVD  43266  syl5impVD  43267  ssralv2VD  43270  ordelordALTVD  43271  equncomVD  43272  imbi12VD  43277  imbi13VD  43278  sbcim2gVD  43279  sbcbiVD  43280  trsbcVD  43281  truniALTVD  43282  trintALTVD  43284  undif3VD  43286  sbcssgVD  43287  csbingVD  43288  onfrALTlem3VD  43291  simplbi2comtVD  43292  onfrALTlem2VD  43293  onfrALTVD  43295  csbeq2gVD  43296  csbsngVD  43297  csbxpgVD  43298  csbresgVD  43299  csbrngVD  43300  csbima12gALTVD  43301  csbunigVD  43302  csbfv12gALTVD  43303  con5VD  43304  relopabVD  43305  19.41rgVD  43306  2pm13.193VD  43307  hbimpgVD  43308  hbalgVD  43309  hbexgVD  43310  ax6e2eqVD  43311  ax6e2ndVD  43312  ax6e2ndeqVD  43313  2sb5ndVD  43314  2uasbanhVD  43315  e2ebindVD  43316  sb5ALTVD  43317  vk15.4jVD  43318  notnotrALTVD  43319  con3ALTVD  43320  sspwimpVD  43323  sspwimpcfVD  43325  suctrALTcfVD  43327