Theorem idn1 44998

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

Syntax hints:  (   wvd1 44993

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 44994

This theorem is referenced by:  trsspwALT  45241  sspwtr  45244  pwtrVD  45247  pwtrrVD  45248  snssiALTVD  45250  snsslVD  45252  snelpwrVD  45254  unipwrVD  45255  sstrALT2VD  45257  suctrALT2VD  45259  elex2VD  45261  elex22VD  45262  eqsbc2VD  45263  zfregs2VD  45264  tpid3gVD  45265  en3lplem1VD  45266  en3lplem2VD  45267  en3lpVD  45268  3ornot23VD  45270  orbi1rVD  45271  3orbi123VD  45273  sbc3orgVD  45274  19.21a3con13vVD  45275  exbirVD  45276  exbiriVD  45277  rspsbc2VD  45278  3impexpVD  45279  3impexpbicomVD  45280  tratrbVD  45284  al2imVD  45285  syl5impVD  45286  ssralv2VD  45289  ordelordALTVD  45290  equncomVD  45291  imbi12VD  45296  imbi13VD  45297  sbcim2gVD  45298  sbcbiVD  45299  trsbcVD  45300  truniALTVD  45301  trintALTVD  45303  undif3VD  45305  sbcssgVD  45306  csbingVD  45307  onfrALTlem3VD  45310  simplbi2comtVD  45311  onfrALTlem2VD  45312  onfrALTVD  45314  csbeq2gVD  45315  csbsngVD  45316  csbxpgVD  45317  csbresgVD  45318  csbrngVD  45319  csbima12gALTVD  45320  csbunigVD  45321  csbfv12gALTVD  45322  con5VD  45323  relopabVD  45324  19.41rgVD  45325  2pm13.193VD  45326  hbimpgVD  45327  hbalgVD  45328  hbexgVD  45329  ax6e2eqVD  45330  ax6e2ndVD  45331  ax6e2ndeqVD  45332  2sb5ndVD  45333  2uasbanhVD  45334  e2ebindVD  45335  sb5ALTVD  45336  vk15.4jVD  45337  notnotrALTVD  45338  con3ALTVD  45339  sspwimpVD  45342  sspwimpcfVD  45344  suctrALTcfVD  45346