Theorem biidd 262

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  ifpbi23d  1080  3anbi12d  1439  3anbi13d  1440  3anbi23d  1441  3anbi1d  1442  3anbi2d  1443  3anbi3d  1444  nfald2  2450  exdistrf  2452  sb6x  2469  axc16gALT  2495  raleqOLD  3340  rexeqOLD  3341  vtoclegft  3588  ralxpxfr2d  3646  rr19.3v  3667  rr19.28v  3668  rabtru  3689  moeq3  3718  euxfr2w  3726  euxfr2  3728  reuxfrd  3754  dfif3  4540  sseliALT  5309  copsexgw  5495  copsexg  5496  soeq1  5613  frd  5641  soinxp  5767  idrefALT  6131  ordtri3or  6416  nfriotadw  7396  oprabidw  7462  ov6g  7597  ovg  7598  sorpssi  7749  dfxp3  8086  fsplit  8142  frxp3  8176  xpord3inddlem  8179  aceq1  10157  aceq2  10159  axpowndlem4  10640  axpownd  10641  ltsopr  11072  creur  12260  creui  12261  o1fsum  15849  sumodd  16425  sadfval  16489  sadcp1  16492  pceu  16884  vdwlem12  17030  sgrp2rid2ex  18940  gsumval3eu  19922  lss1d  20961  nrmr0reg  23757  stdbdxmet  24528  xrsxmet  24831  cmetcaulem  25322  bcth3  25365  iundisj2  25584  ulmdvlem3  26445  ulmdv  26446  dchrvmasumlem2  27542  colrot1  28567  lnrot1  28631  lnrot2  28632  wlkson  29674  trlsfval  29713  pthsfval  29739  spthsfval  29740  clwlks  29792  crcts  29808  cycls  29809  3cyclfrgrrn1  30304  frgrwopreg  30342  reuxfrdf  32510  iundisj2f  32603  iundisj2fi  32799  ordtprsuni  33918  pmeasmono  34326  erdszelem9  35204  satfv1fvfmla1  35428  opnrebl2  36322  wl-ifpimpr  37467  wl-df-3xor  37469  wl-ax11-lem9  37594  ax12fromc15  38906  axc16g-o  38935  ax12indalem  38946  ax12inda2ALT  38947  dihopelvalcpre  41250  lpolconN  41489  dvrelog2b  42067  isprimroot  42094  aks6d1c2p2  42120  hashscontpow  42123  rspcsbnea  42132  aks6d1c6lem3  42173  fsuppind  42600  zindbi  42958  cnvtrucl0  43637  ismnushort  44320  e2ebind  44583  uunT1  44800  ovnval2  46560  ovnval2b  46567  hoiqssbl  46640  6gbe  47758  8gbe  47760  isgrim  47868  usgrexmpl1tri  47984  gpgov  48001  gpg3kgrtriex  48045