Theorem biidd 265

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ifpbi23d  1082  3anbi12d  1439  3anbi13d  1440  3anbi23d  1441  3anbi1d  1442  3anbi2d  1443  3anbi3d  1444  nfald2  2444  exdistrf  2446  sb6x  2463  axc16gALT  2493  raleq  3309  rexeq  3310  ralxpxfr2d  3543  rr19.3v  3566  rr19.28v  3567  rabtru  3588  moeq3  3614  euxfr2w  3622  euxfr2  3624  reuxfrd  3650  dfif3  4439  sseliALT  5187  copsexgw  5358  copsexg  5359  soeq1  5474  soinxp  5615  idrefALT  5958  ordtri3or  6223  nfriotadw  7156  oprabidw  7222  ov6g  7350  ovg  7351  sorpssi  7495  dfxp3  7809  fsplit  7863  aceq1  9696  aceq2  9698  axpowndlem4  10179  axpownd  10180  ltsopr  10611  creur  11789  creui  11790  o1fsum  15340  sumodd  15912  sadfval  15974  sadcp1  15977  pceu  16362  vdwlem12  16508  sgrp2rid2ex  18308  gsumval3eu  19243  lss1d  19954  nrmr0reg  22600  stdbdxmet  23367  xrsxmet  23660  cmetcaulem  24139  bcth3  24182  iundisj2  24400  ulmdvlem3  25248  ulmdv  25249  dchrvmasumlem2  26333  colrot1  26604  lnrot1  26668  lnrot2  26669  wlkson  27698  trlsfval  27737  pthsfval  27762  spthsfval  27763  clwlks  27813  crcts  27829  cycls  27830  3cyclfrgrrn1  28322  frgrwopreg  28360  reuxfrdf  30512  iundisj2f  30602  iundisj2fi  30792  ordtprsuni  31537  pmeasmono  31957  erdszelem9  32828  satfv1fvfmla1  33052  xpord3ind  33480  opnrebl2  34196  wl-ifpimpr  35323  wl-df-3xor  35325  wl-ax11-lem9  35430  ax12fromc15  36605  axc16g-o  36634  ax12indalem  36645  ax12inda2ALT  36646  dihopelvalcpre  38948  lpolconN  39187  dvrelog2b  39756  sticksstones11  39781  fsuppind  39930  zindbi  40412  cnvtrucl0  40849  ismnushort  41533  e2ebind  41797  uunT1  42014  ovnval2  43701  ovnval2b  43708  hoiqssbl  43781  6gbe  44839  8gbe  44841