Theorem biidd 251

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 250	. 2 ⊢ (𝜓 ↔ 𝜓)
2	1	a1i 11	1 ⊢ (𝜑 → (𝜓 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 195

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

This theorem is referenced by:  3anbi12d  1392  3anbi13d  1393  3anbi23d  1394  3anbi1d  1395  3anbi2d  1396  3anbi3d  1397  nfald2  2319  exdistrf  2321  ax12OLD  2329  axc16gALT  2355  sb6x  2372  ralxpxfr2d  3298  rr19.3v  3314  rr19.28v  3315  moeq3  3350  euxfr2  3358  dfif3  4050  sseliALT  4719  reuxfr2d  4817  copsexg  4882  soeq1  4978  soinxp  5106  ordtri3or  5672  ov6g  6696  ovg  6697  sorpssi  6841  dfxp3  7119  aceq1  8823  aceq2  8825  axpowndlem4  9301  axpownd  9302  ltsopr  9733  creur  10891  creui  10892  o1fsum  14386  sumodd  14949  sadfval  15012  sadcp1  15015  pceu  15389  vdwlem12  15534  sgrp2rid2ex  17237  gsumval3eu  18128  lss1d  18784  nrmr0reg  21362  stdbdxmet  22130  xrsxmet  22420  cmetcaulem  22894  bcth3  22936  iundisj2  23124  ulmdvlem3  23960  ulmdv  23961  dchrvmasumlem2  24987  colrot1  25254  lnrot1  25318  lnrot2  25319  dfcgra2  25521  isinag  25529  2pthoncl  26133  crcts  26150  cycls  26151  3cyclfrgrarn1  26539  frgraregorufr0  26579  reuxfr3d  28713  rabtru  28723  iundisj2f  28785  iundisj2fi  28943  ordtprsuni  29293  isrnsigaOLD  29502  pmeasmono  29713  erdszelem9  30435  opnrebl2  31486  wl-ax11-lem9  32549  ax12fromc15  33208  axc16g-o  33237  ax12indalem  33248  ax12inda2ALT  33249  dihopelvalcpre  35555  lpolconN  35794  zindbi  36529  cnvtrucl0  36950  e2ebind  37800  uunT1  38028  trsbcVD  38135  ovnval2  39435  ovnval2b  39442  hoiqssbl  39515  6gbe  40193  8gbe  40195  isrusgr  40761  1wlksfval  40811  wlkson  40864  trlsfval  40903  pthsfval  40927  spthsfval  40928  clwlkS  40978  crctS  40994  cyclS  40995  isfrgr  41430  3cyclfrgrrn1  41455  frgrregorufr0  41489