Theorem biidd 253

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

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  3anbi12d  1554  3anbi13d  1555  3anbi23d  1556  3anbi1d  1557  3anbi2d  1558  3anbi3d  1559  nfald2  2493  exdistrf  2495  axc16gALT  2526  sb6x  2543  ralxpxfr2d  3521  rr19.3v  3540  rr19.28v  3541  rabtru  3556  moeq3  3581  euxfr2  3589  dfif3  4293  sseliALT  4986  reuxfr2d  5088  copsexg  5145  soeq1  5251  soinxp  5385  idrefALT  5719  ordtri3or  5968  ov6g  7028  ovg  7029  sorpssi  7173  dfxp3  7463  aceq1  9223  aceq2  9225  axpowndlem4  9707  axpownd  9708  ltsopr  10139  creur  11299  creui  11300  o1fsum  14767  sumodd  15331  sadfval  15393  sadcp1  15396  pceu  15768  vdwlem12  15913  sgrp2rid2ex  17619  gsumval3eu  18506  lss1d  19170  nrmr0reg  21766  stdbdxmet  22533  xrsxmet  22825  cmetcaulem  23298  bcth3  23340  iundisj2  23530  ulmdvlem3  24370  ulmdv  24371  dchrvmasumlem2  25401  colrot1  25668  lnrot1  25732  lnrot2  25733  dfcgra2  25935  isinag  25943  isrusgr  26685  wksfval  26733  wlkson  26780  trlsfval  26820  pthsfval  26845  spthsfval  26846  clwlks  26896  crcts  26912  cycls  26913  3cyclfrgrrn1  27460  frgrwopreg  27498  reuxfr3d  29655  iundisj2f  29728  iundisj2fi  29883  ordtprsuni  30290  isrnsigaOLD  30500  pmeasmono  30711  erdszelem9  31504  opnrebl2  32637  wl-ax11-lem9  33684  ax12fromc15  34684  axc16g-o  34713  ax12indalem  34724  ax12inda2ALT  34725  dihopelvalcpre  37029  lpolconN  37268  zindbi  38012  cnvtrucl0  38431  e2ebind  39277  uunT1  39504  trsbcVD  39607  ovnval2  41241  ovnval2b  41248  hoiqssbl  41321  6gbe  42234  8gbe  42236