Theorem idn1 37811

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

Syntax hints:  (   wvd1 37806

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 196  df-vd1 37807

This theorem is referenced by:  trsspwALT  38067  sspwtr  38070  pwtrVD  38081  pwtrrVD  38082  snssiALTVD  38084  snsslVD  38086  snelpwrVD  38088  unipwrVD  38089  sstrALT2VD  38091  suctrALT2VD  38093  elex2VD  38095  elex22VD  38096  eqsbc3rVD  38097  zfregs2VD  38098  tpid3gVD  38099  en3lplem1VD  38100  en3lplem2VD  38101  en3lpVD  38102  3ornot23VD  38104  orbi1rVD  38105  3orbi123VD  38107  sbc3orgVD  38108  19.21a3con13vVD  38109  exbirVD  38110  exbiriVD  38111  rspsbc2VD  38112  3impexpVD  38113  3impexpbicomVD  38114  sbcoreleleqVD  38117  tratrbVD  38119  al2imVD  38120  syl5impVD  38121  ssralv2VD  38124  ordelordALTVD  38125  equncomVD  38126  imbi12VD  38131  imbi13VD  38132  sbcim2gVD  38133  sbcbiVD  38134  trsbcVD  38135  truniALTVD  38136  trintALTVD  38138  undif3VD  38140  sbcssgVD  38141  csbingVD  38142  onfrALTlem3VD  38145  simplbi2comtVD  38146  onfrALTlem2VD  38147  onfrALTVD  38149  csbeq2gVD  38150  csbsngVD  38151  csbxpgVD  38152  csbresgVD  38153  csbrngVD  38154  csbima12gALTVD  38155  csbunigVD  38156  csbfv12gALTVD  38157  con5VD  38158  relopabVD  38159  19.41rgVD  38160  2pm13.193VD  38161  hbimpgVD  38162  hbalgVD  38163  hbexgVD  38164  ax6e2eqVD  38165  ax6e2ndVD  38166  ax6e2ndeqVD  38167  2sb5ndVD  38168  2uasbanhVD  38169  e2ebindVD  38170  sb5ALTVD  38171  vk15.4jVD  38172  notnotrALTVD  38173  con3ALTVD  38174  sspwimpVD  38177  sspwimpcfVD  38179  suctrALTcfVD  38181