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 ⊢ (𝜑 → (𝜓 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  ifpbi23d  1096  3anbi12d  1465  3anbi13d  1466  3anbi23d  1467  3anbi1d  1468  3anbi2d  1469  3anbi3d  1470  nfald2  2474  exdistrf  2476  sb6x  2493  axc16gALT  2519  vtoclegft  3543  ralxpxfr2d  3599  rr19.3v  3620  rr19.28v  3621  rabtru  3642  moeq3  3669  euxfr2w  3677  euxfr2  3679  reuxfrd  3705  vn0  4290  vn0OLD  4291  eq0  4296  ab0orv  4331  dfif3  4496  sseliALT  5262  copsexgwOLD  5460  copsexg  5461  soeq1  5579  frd  5607  soinxp  5732  idrefALT  6106  ordtri3or  6395  nfriotadw  7386  oprabidw  7452  ov6g  7585  ovg  7586  sorpssi  7746  dfxp3  8073  fsplit  8131  frxp3  8171  xpord3inddlem  8174  aceq1  10200  aceq2  10202  axpowndlem4  10689  axpownd  10690  ltsopr  11121  creur  12318  creui  12319  o1fsum  15986  sumodd  16564  sadfval  16628  sadcp1  16631  pceu  17030  vdwlem12  17176  sgrp2rid2ex  19132  gsumval3eu  20124  lss1d  21244  nrmr0reg  24074  stdbdxmet  24840  xrsxmet  25135  cmetcaulem  25615  bcth3  25658  iundisj2  25876  ulmdvlem3  26735  ulmdv  26736  dchrvmasumlem2  27831  colrot1  29028  lnrot1  29097  lnrot2  29098  tgplnfn  29259  plngval  29261  isplng  29262  elcgrabasi  29381  wlkson  30241  trlsfval  30284  pthsfval  30310  spthsfval  30311  clwlks  30365  crcts  30381  cycls  30382  3cyclfrgrrn1  30892  frgrwopreg  30930  reuxfrdf  33135  iundisj2f  33232  iundisj2fi  33436  constrcbvlem  34434  ordtprsuni  34598  pmeasmono  35003  erdszelem9  36051  satfv1fvfmla1  36275  opnrebl2  37202  wl-ifpimpr  38483  wl-df-3xor  38485  ax12fromc15  40056  axc16g-o  40085  ax12indalem  40096  ax12inda2ALT  40097  dihopelvalcpre  42399  lpolconN  42638  dvrelog2b  43210  isprimroot  43237  aks6d1c2p2  43263  hashscontpow  43266  rspcsbnea  43275  aks6d1c6lem3  43316  fsuppind  43712  zindbi  44047  cnvtrucl0  44718  ismnushort  45379  e2ebind  45640  uunT1  45856  ovnval2  47649  ovnval2b  47656  hoiqssbl  47729  6gbe  48963  8gbe  48965  isgrim  49074  usgrexmpl1tri  49217  gpgov  49234  gpg3kgrtriex  49281