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  2476  exdistrf  2478  sb6x  2495  axc16gALT  2521  vtoclegft  3546  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  5270  copsexgwOLD  5471  copsexg  5472  soeq1  5588  frd  5616  soinxp  5741  idrefALT  6111  ordtri3or  6394  nfriotadw  7382  oprabidw  7448  ov6g  7581  ovg  7582  sorpssi  7734  dfxp3  8062  fsplit  8118  frxp3  8153  xpord3inddlem  8156  aceq1  10124  aceq2  10126  axpowndlem4  10613  axpownd  10614  ltsopr  11045  creur  12240  creui  12241  o1fsum  15904  sumodd  16484  sadfval  16548  sadcp1  16551  pceu  16944  vdwlem12  17090  sgrp2rid2ex  19045  gsumval3eu  20037  lss1d  21153  nrmr0reg  23981  stdbdxmet  24747  xrsxmet  25042  cmetcaulem  25522  bcth3  25565  iundisj2  25783  ulmdvlem3  26645  ulmdv  26646  dchrvmasumlem2  27742  colrot1  28909  lnrot1  28978  lnrot2  28979  tgplnfn  29140  plngval  29142  isplng  29143  elcgrabasi  29262  wlkson  30122  trlsfval  30165  pthsfval  30191  spthsfval  30192  clwlks  30246  crcts  30262  cycls  30263  3cyclfrgrrn1  30773  frgrwopreg  30811  reuxfrdf  32974  iundisj2f  33071  iundisj2fi  33276  constrcbvlem  34273  ordtprsuni  34437  pmeasmono  34843  erdszelem9  35786  satfv1fvfmla1  36010  opnrebl2  36948  wl-ifpimpr  38228  wl-df-3xor  38230  ax12fromc15  39786  axc16g-o  39815  ax12indalem  39826  ax12inda2ALT  39827  dihopelvalcpre  42129  lpolconN  42368  dvrelog2b  42940  isprimroot  42967  aks6d1c2p2  42993  hashscontpow  42996  rspcsbnea  43005  aks6d1c6lem3  43046  fsuppind  43444  zindbi  43795  cnvtrucl0  44472  ismnushort  45133  e2ebind  45394  uunT1  45610  ovnval2  47381  ovnval2b  47388  hoiqssbl  47461  6gbe  48695  8gbe  48697  isgrim  48806  usgrexmpl1tri  48949  gpgov  48966  gpg3kgrtriex  49013