Theorem idn1 44852

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

Syntax hints:  (   wvd1 44847

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 44848

This theorem is referenced by:  trsspwALT  45095  sspwtr  45098  pwtrVD  45101  pwtrrVD  45102  snssiALTVD  45104  snsslVD  45106  snelpwrVD  45108  unipwrVD  45109  sstrALT2VD  45111  suctrALT2VD  45113  elex2VD  45115  elex22VD  45116  eqsbc2VD  45117  zfregs2VD  45118  tpid3gVD  45119  en3lplem1VD  45120  en3lplem2VD  45121  en3lpVD  45122  3ornot23VD  45124  orbi1rVD  45125  3orbi123VD  45127  sbc3orgVD  45128  19.21a3con13vVD  45129  exbirVD  45130  exbiriVD  45131  rspsbc2VD  45132  3impexpVD  45133  3impexpbicomVD  45134  tratrbVD  45138  al2imVD  45139  syl5impVD  45140  ssralv2VD  45143  ordelordALTVD  45144  equncomVD  45145  imbi12VD  45150  imbi13VD  45151  sbcim2gVD  45152  sbcbiVD  45153  trsbcVD  45154  truniALTVD  45155  trintALTVD  45157  undif3VD  45159  sbcssgVD  45160  csbingVD  45161  onfrALTlem3VD  45164  simplbi2comtVD  45165  onfrALTlem2VD  45166  onfrALTVD  45168  csbeq2gVD  45169  csbsngVD  45170  csbxpgVD  45171  csbresgVD  45172  csbrngVD  45173  csbima12gALTVD  45174  csbunigVD  45175  csbfv12gALTVD  45176  con5VD  45177  relopabVD  45178  19.41rgVD  45179  2pm13.193VD  45180  hbimpgVD  45181  hbalgVD  45182  hbexgVD  45183  ax6e2eqVD  45184  ax6e2ndVD  45185  ax6e2ndeqVD  45186  2sb5ndVD  45187  2uasbanhVD  45188  e2ebindVD  45189  sb5ALTVD  45190  vk15.4jVD  45191  notnotrALTVD  45192  con3ALTVD  45193  sspwimpVD  45196  sspwimpcfVD  45198  suctrALTcfVD  45200