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  4714  reuxfr2d  4812  copsexg  4876  soeq1  4968  soinxp  5096  ordtri3or  5658  ov6g  6674  ovg  6675  sorpssi  6819  dfxp3  7097  aceq1  8801  aceq2  8803  axpowndlem4  9279  axpownd  9280  ltsopr  9711  creur  10864  creui  10865  o1fsum  14335  sumodd  14898  sadfval  14961  sadcp1  14964  pceu  15338  vdwlem12  15483  sgrp2rid2ex  17186  gsumval3eu  18077  lss1d  18733  nrmr0reg  21310  stdbdxmet  22078  xrsxmet  22368  cmetcaulem  22839  bcth3  22881  iundisj2  23069  ulmdvlem3  23905  ulmdv  23906  dchrvmasumlem2  24932  colrot1  25200  lnrot1  25264  lnrot2  25265  dfcgra2  25467  isinag  25475  2pthoncl  25927  crcts  25944  cycls  25945  3cyclfrgrarn1  26333  frgraregorufr0  26373  reuxfr3d  28507  rabtru  28517  iundisj2f  28579  iundisj2fi  28737  ordtprsuni  29087  isrnsigaOLD  29296  pmeasmono  29507  erdszelem9  30229  opnrebl2  31280  wl-ax11-lem9  32343  ax12fromc15  33002  axc16g-o  33031  ax12indalem  33042  ax12inda2ALT  33043  dihopelvalcpre  35349  lpolconN  35588  zindbi  36323  cnvtrucl0  36744  e2ebind  37594  uunT1  37822  trsbcVD  37929  ovnval2  39229  ovnval2b  39236  hoiqssbl  39309  6gbe  39988  8gbe  39990  isrusgr  40753  1wlksfval  40803  wlkson  40856  trlsfval  40895  pthsfval  40919  spthsfval  40920  clwlkS  40970  crctS  40986  cyclS  40987  isfrgr  41422  3cyclfrgrrn1  41447  frgrregorufr0  41481