Theorem biidd 252

Description: Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.)

Assertion

Ref	Expression
biidd	⊢ (𝜑 → (𝜓 ↔ 𝜓))

Proof of Theorem biidd

Step	Hyp	Ref	Expression
1		biid 251	. 2 ⊢ (𝜓 ↔ 𝜓)
2	1	a1i 11	1 ⊢ (𝜑 → (𝜓 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  3anbi12d  1400  3anbi13d  1401  3anbi23d  1402  3anbi1d  1403  3anbi2d  1404  3anbi3d  1405  nfald2  2331  exdistrf  2333  ax12OLD  2341  axc16gALT  2367  sb6x  2384  ralxpxfr2d  3327  rr19.3v  3345  rr19.28v  3346  rabtru  3361  moeq3  3383  euxfr2  3391  dfif3  4100  sseliALT  4791  reuxfr2d  4891  copsexg  4956  soeq1  5054  soinxp  5183  ordtri3or  5755  ov6g  6798  ovg  6799  sorpssi  6943  dfxp3  7230  aceq1  8940  aceq2  8942  axpowndlem4  9422  axpownd  9423  ltsopr  9854  creur  11014  creui  11015  o1fsum  14545  sumodd  15111  sadfval  15174  sadcp1  15177  pceu  15551  vdwlem12  15696  sgrp2rid2ex  17414  gsumval3eu  18305  lss1d  18963  nrmr0reg  21552  stdbdxmet  22320  xrsxmet  22612  cmetcaulem  23086  bcth3  23128  iundisj2  23317  ulmdvlem3  24156  ulmdv  24157  dchrvmasumlem2  25187  colrot1  25454  lnrot1  25518  lnrot2  25519  dfcgra2  25721  isinag  25729  isrusgr  26457  wksfval  26505  wlkson  26552  trlsfval  26592  pthsfval  26617  spthsfval  26618  clwlks  26668  crcts  26683  cycls  26684  3cyclfrgrrn1  27149  frgrwopreg  27187  reuxfr3d  29329  iundisj2f  29403  iundisj2fi  29556  ordtprsuni  29965  isrnsigaOLD  30175  pmeasmono  30386  erdszelem9  31181  opnrebl2  32316  wl-ax11-lem9  33370  ax12fromc15  34190  axc16g-o  34219  ax12indalem  34230  ax12inda2ALT  34231  dihopelvalcpre  36537  lpolconN  36776  zindbi  37511  cnvtrucl0  37931  e2ebind  38779  uunT1  39007  trsbcVD  39113  ovnval2  40759  ovnval2b  40766  hoiqssbl  40839  6gbe  41659  8gbe  41661