Theorem biidd 263

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  ifpbi23d  1085  3anbi12d  1445  3anbi13d  1446  3anbi23d  1447  3anbi1d  1448  3anbi2d  1449  3anbi3d  1450  nfald2  2453  exdistrf  2455  sb6x  2472  axc16gALT  2498  vtoclegft  3534  ralxpxfr2d  3591  rr19.3v  3612  rr19.28v  3613  rabtru  3634  moeq3  3660  euxfr2w  3668  euxfr2  3670  reuxfrd  3696  vn0  4280  eq0  4285  ab0orv  4318  dfif3  4476  sseliALT  5238  copsexgwOLD  5438  copsexg  5439  soeq1  5554  frd  5582  soinxp  5707  idrefALT  6070  ordtri3or  6349  nfriotadw  7328  oprabidw  7394  ov6g  7527  ovg  7528  sorpssi  7679  dfxp3  8010  fsplit  8063  frxp3  8098  xpord3inddlem  8101  aceq1  10037  aceq2  10039  axpowndlem4  10521  axpownd  10522  ltsopr  10953  creur  12151  creui  12152  o1fsum  15774  sumodd  16355  sadfval  16419  sadcp1  16422  pceu  16815  vdwlem12  16961  sgrp2rid2ex  18896  gsumval3eu  19877  lss1d  20960  nrmr0reg  23739  stdbdxmet  24505  xrsxmet  24800  cmetcaulem  25280  bcth3  25323  iundisj2  25541  ulmdvlem3  26392  ulmdv  26393  dchrvmasumlem2  27486  colrot1  28652  lnrot1  28716  lnrot2  28717  wlkson  29748  trlsfval  29787  pthsfval  29812  spthsfval  29813  clwlks  29865  crcts  29881  cycls  29882  3cyclfrgrrn1  30380  frgrwopreg  30418  reuxfrdf  32585  iundisj2f  32686  iundisj2fi  32896  constrcbvlem  33946  ordtprsuni  34110  pmeasmono  34515  erdszelem9  35434  satfv1fvfmla1  35658  opnrebl2  36556  wl-ifpimpr  37835  wl-df-3xor  37837  ax12fromc15  39404  axc16g-o  39433  ax12indalem  39444  ax12inda2ALT  39445  dihopelvalcpre  41747  lpolconN  41986  dvrelog2b  42558  isprimroot  42585  aks6d1c2p2  42611  hashscontpow  42614  rspcsbnea  42623  aks6d1c6lem3  42664  fsuppind  43047  zindbi  43398  cnvtrucl0  44075  ismnushort  44752  e2ebind  45014  uunT1  45230  ovnval2  46995  ovnval2b  47002  hoiqssbl  47075  6gbe  48269  8gbe  48271  isgrim  48380  usgrexmpl1tri  48523  gpgov  48540  gpg3kgrtriex  48587