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  1466  3anbi13d  1467  3anbi23d  1468  3anbi1d  1469  3anbi2d  1470  3anbi3d  1471  nfald2  2477  exdistrf  2479  sb6x  2496  axc16gALT  2522  vtoclegft  3547  ralxpxfr2d  3603  rr19.3v  3624  rr19.28v  3625  rabtru  3646  moeq3  3673  euxfr2w  3681  euxfr2  3683  reuxfrd  3709  vn0  4294  vn0OLD  4295  eq0  4300  ab0orv  4335  dfif3  4500  sseliALT  5267  copsexgwOLD  5466  copsexg  5467  soeq1  5585  frd  5613  soinxp  5739  idrefALT  6120  ordtri3or  6416  nfriotadw  7411  oprabidw  7477  ov6g  7611  ovg  7612  sorpssi  7772  dfxp3  8100  fsplit  8158  frxp3  8198  xpord3inddlem  8201  aceq1  10226  aceq2  10228  axpowndlem4  10715  axpownd  10716  ltsopr  11147  creur  12344  creui  12345  o1fsum  16012  sumodd  16590  sadfval  16654  sadcp1  16657  pceu  17056  vdwlem12  17202  sgrp2rid2ex  19158  gsumval3eu  20151  lss1d  21271  nrmr0reg  24101  stdbdxmet  24867  xrsxmet  25162  cmetcaulem  25642  bcth3  25685  iundisj2  25903  ulmdvlem3  26762  ulmdv  26763  dchrvmasumlem2  27858  colrot1  29055  lnrot1  29124  lnrot2  29125  tgplnfn  29286  plngval  29288  isplng  29289  elcgrabasi  29408  wlkson  30268  trlsfval  30311  pthsfval  30337  spthsfval  30338  clwlks  30392  crcts  30408  cycls  30409  3cyclfrgrrn1  30919  frgrwopreg  30957  reuxfrdf  33162  iundisj2f  33259  iundisj2fi  33462  constrcbvlem  34470  ordtprsuni  34634  pmeasmono  35039  erdszelem9  36144  satfv1fvfmla1  36368  opnrebl2  37300  wl-ifpimpr  38594  wl-df-3xor  38596  ax12fromc15  40165  axc16g-o  40194  ax12indalem  40205  ax12inda2ALT  40206  dihopelvalcpre  42508  lpolconN  42747  dvrelog2b  43319  isprimroot  43346  aks6d1c2p2  43372  hashscontpow  43375  rspcsbnea  43384  aks6d1c6lem3  43425  fsuppind  43822  zindbi  44157  cnvtrucl0  44827  ismnushort  45488  e2ebind  45748  uunT1  45964  ovnval2  47770  ovnval2b  47777  hoiqssbl  47850  6gbe  49084  8gbe  49086  isgrim  49195  usgrexmpl1tri  49338  gpgov  49355  gpg3kgrtriex  49402