Theorem idn1 45384

Description: Virtual deduction identity rule which is id 23 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 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	dfvd1ir 45383	1 ⊢ (   𝜑   ▶   𝜑   )

This proof depends on syntax axioms:  (   wvd1 45379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-vd1 45380

This theorem is used by:  trsspwALT  45627  sspwtr  45630  pwtrVD  45633  pwtrrVD  45634  snssiALTVD  45636  snsslVD  45638  snelpwrVD  45640  unipwrVD  45641  sstrALT2VD  45643  suctrALT2VD  45645  elex2VD  45647  elex22VD  45648  eqsbc2VD  45649  zfregs2VD  45650  tpid3gVD  45651  en3lplem1VD  45652  en3lplem2VD  45653  en3lpVD  45654  3ornot23VD  45656  orbi1rVD  45657  3orbi123VD  45659  sbc3orgVD  45660  19.21a3con13vVD  45661  exbirVD  45662  exbiriVD  45663  rspsbc2VD  45664  3impexpVD  45665  3impexpbicomVD  45666  tratrbVD  45670  al2imVD  45671  syl5impVD  45672  ssralv2VD  45675  ordelordALTVD  45676  equncomVD  45677  imbi12VD  45682  imbi13VD  45683  sbcim2gVD  45684  sbcbiVD  45685  trsbcVD  45686  truniALTVD  45687  trintALTVD  45689  undif3VD  45691  sbcssgVD  45692  csbingVD  45693  onfrALTlem3VD  45696  simplbi2comtVD  45697  onfrALTlem2VD  45698  onfrALTVD  45700  csbeq2gVD  45701  csbsngVD  45702  csbxpgVD  45703  csbresgVD  45704  csbrngVD  45705  csbima12gALTVD  45706  csbunigVD  45707  csbfv12gALTVD  45708  con5VD  45709  relopabVD  45710  19.41rgVD  45711  2pm13.193VD  45712  hbimpgVD  45713  hbalgVD  45714  hbexgVD  45715  ax6e2eqVD  45716  ax6e2ndVD  45717  ax6e2ndeqVD  45718  2sb5ndVD  45719  2uasbanhVD  45720  e2ebindVD  45721  sb5ALTVD  45722  vk15.4jVD  45723  notnotrALTVD  45724  con3ALTVD  45725  sspwimpVD  45728  sspwimpcfVD  45730  suctrALTcfVD  45732