Theorem idn1 43926

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

Syntax hints:  (   wvd1 43921

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 43922

This theorem is referenced by:  trsspwALT  44170  sspwtr  44173  pwtrVD  44176  pwtrrVD  44177  snssiALTVD  44179  snsslVD  44181  snelpwrVD  44183  unipwrVD  44184  sstrALT2VD  44186  suctrALT2VD  44188  elex2VD  44190  elex22VD  44191  eqsbc2VD  44192  zfregs2VD  44193  tpid3gVD  44194  en3lplem1VD  44195  en3lplem2VD  44196  en3lpVD  44197  3ornot23VD  44199  orbi1rVD  44200  3orbi123VD  44202  sbc3orgVD  44203  19.21a3con13vVD  44204  exbirVD  44205  exbiriVD  44206  rspsbc2VD  44207  3impexpVD  44208  3impexpbicomVD  44209  tratrbVD  44213  al2imVD  44214  syl5impVD  44215  ssralv2VD  44218  ordelordALTVD  44219  equncomVD  44220  imbi12VD  44225  imbi13VD  44226  sbcim2gVD  44227  sbcbiVD  44228  trsbcVD  44229  truniALTVD  44230  trintALTVD  44232  undif3VD  44234  sbcssgVD  44235  csbingVD  44236  onfrALTlem3VD  44239  simplbi2comtVD  44240  onfrALTlem2VD  44241  onfrALTVD  44243  csbeq2gVD  44244  csbsngVD  44245  csbxpgVD  44246  csbresgVD  44247  csbrngVD  44248  csbima12gALTVD  44249  csbunigVD  44250  csbfv12gALTVD  44251  con5VD  44252  relopabVD  44253  19.41rgVD  44254  2pm13.193VD  44255  hbimpgVD  44256  hbalgVD  44257  hbexgVD  44258  ax6e2eqVD  44259  ax6e2ndVD  44260  ax6e2ndeqVD  44261  2sb5ndVD  44262  2uasbanhVD  44263  e2ebindVD  44264  sb5ALTVD  44265  vk15.4jVD  44266  notnotrALTVD  44267  con3ALTVD  44268  sspwimpVD  44271  sspwimpcfVD  44273  suctrALTcfVD  44275