Theorem idn1 44893

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

Syntax hints:  (   wvd1 44888

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 44889

This theorem is referenced by:  trsspwALT  45136  sspwtr  45139  pwtrVD  45142  pwtrrVD  45143  snssiALTVD  45145  snsslVD  45147  snelpwrVD  45149  unipwrVD  45150  sstrALT2VD  45152  suctrALT2VD  45154  elex2VD  45156  elex22VD  45157  eqsbc2VD  45158  zfregs2VD  45159  tpid3gVD  45160  en3lplem1VD  45161  en3lplem2VD  45162  en3lpVD  45163  3ornot23VD  45165  orbi1rVD  45166  3orbi123VD  45168  sbc3orgVD  45169  19.21a3con13vVD  45170  exbirVD  45171  exbiriVD  45172  rspsbc2VD  45173  3impexpVD  45174  3impexpbicomVD  45175  tratrbVD  45179  al2imVD  45180  syl5impVD  45181  ssralv2VD  45184  ordelordALTVD  45185  equncomVD  45186  imbi12VD  45191  imbi13VD  45192  sbcim2gVD  45193  sbcbiVD  45194  trsbcVD  45195  truniALTVD  45196  trintALTVD  45198  undif3VD  45200  sbcssgVD  45201  csbingVD  45202  onfrALTlem3VD  45205  simplbi2comtVD  45206  onfrALTlem2VD  45207  onfrALTVD  45209  csbeq2gVD  45210  csbsngVD  45211  csbxpgVD  45212  csbresgVD  45213  csbrngVD  45214  csbima12gALTVD  45215  csbunigVD  45216  csbfv12gALTVD  45217  con5VD  45218  relopabVD  45219  19.41rgVD  45220  2pm13.193VD  45221  hbimpgVD  45222  hbalgVD  45223  hbexgVD  45224  ax6e2eqVD  45225  ax6e2ndVD  45226  ax6e2ndeqVD  45227  2sb5ndVD  45228  2uasbanhVD  45229  e2ebindVD  45230  sb5ALTVD  45231  vk15.4jVD  45232  notnotrALTVD  45233  con3ALTVD  45234  sspwimpVD  45237  sspwimpcfVD  45239  suctrALTcfVD  45241