Theorem biid 250

Description: Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117. This is part of Frege's eighth axiom per Proposition 54 of [Frege1879] p. 50; see also eqid 2610. (Contributed by NM, 2-Jun-1993.)

Assertion

Ref	Expression
biid	⊢ (𝜑 ↔ 𝜑)

Proof of Theorem biid

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2	1, 1	impbii 198	1 ⊢ (𝜑 ↔ 𝜑)

Syntax hints:   ↔ wb 195

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 196

This theorem is referenced by:  biidd  251  pm5.19  374  3anbi1i  1246  3anbi2i  1247  3anbi3i  1248  trubitru  1511  falbifal  1514  hadcoma  1529  hadcomb  1530  eqid  2610  abid1  2731  ceqsexg  3304  wecmpep  5030  sorpss  6840  ordon  6874  tz7.49c  7428  dford2  8400  infxpen  8720  isacn  8750  dfac5  8834  dfackm  8871  pwfseq  9365  axgroth5  9525  axgroth6  9529  supmul  10872  fsum2d  14344  cbvprod  14484  fprod2d  14550  rpnnen2lem12  14793  isstruct  15705  oppccatid  16202  subccatid  16329  fuccatid  16452  setccatid  16557  catccatid  16575  estrccatid  16595  xpccatid  16651  lubfun  16803  lubeldm  16804  lubelss  16805  lubval  16807  lubcl  16808  lubprop  16809  lublecl  16812  lubid  16813  glbfun  16816  glbeldm  16817  glbelss  16818  glbval  16820  glbcl  16821  glbprop  16822  joinval2  16832  joineu  16833  meetval2  16846  meeteu  16847  isglbd  16940  lubun  16946  meet0  16960  join0  16961  oduglb  16962  odulub  16964  poslubd  16971  symgsssg  17710  symgfisg  17711  pmtr3ncomlem1  17716  opprsubg  18459  abvtriv  18664  lmodvscl  18703  opsrtos  19307  iscnp2  20853  cbvditg  23424  ditgsplit  23431  lgsquad2  24911  nb3grapr  25982  frgra3v  26529  eqid1  26715  grpoidinv  26746  stri  28500  hstri  28508  stcltrthi  28521  nmo  28709  elxrge02  28971  toslub  28999  tosglb  29001  xrsclat  29011  slmdvscl  29098  unelldsys  29548  omssubadd  29689  ballotlemimin  29894  ballotlemfrcn0  29918  sgnneg  29929  bnj1383  30156  bnj1386  30158  bnj153  30204  bnj543  30217  bnj544  30218  bnj546  30220  bnj605  30231  bnj579  30238  bnj600  30243  bnj601  30244  bnj852  30245  bnj893  30252  bnj906  30254  bnj917  30258  bnj938  30261  bnj944  30262  bnj998  30280  bnj1006  30283  bnj1029  30290  bnj1034  30292  bnj1124  30310  bnj1128  30312  bnj1127  30313  bnj1125  30314  bnj1147  30316  bnj1190  30330  bnj69  30332  bnj1204  30334  bnj1311  30346  bnj1318  30347  bnj1384  30354  bnj1408  30358  bnj1414  30359  bnj1415  30360  bnj1421  30364  bnj1423  30373  bnj1489  30378  bnj1493  30381  bnj60  30384  bnj1500  30390  bnj1522  30394  cvmliftlem11  30531  socnv  30908  dfon2  30941  sltsolem1  31067  brpprod3b  31164  brapply  31215  brrestrict  31226  dfrdg4  31228  cgr3permute3  31324  cgr3permute1  31325  cgr3permute2  31326  cgr3permute4  31327  cgr3permute5  31328  colinearxfr  31352  brsegle  31385  bj-ssbequ2  31832  bj-abid2  31970  bj-termab  32039  bj-restuni  32231  wl-equsal1t  32506  bicontr  33049  elimhyps  33265  lub0N  33494  glb0N  33498  glbconN  33681  dalemeea  33967  dalem4  33969  dalem6  33972  dalem7  33973  dalem11  33978  dalem12  33979  dalem29  34005  dalem30  34006  dalem31N  34007  dalem32  34008  dalem33  34009  dalem34  34010  dalem35  34011  dalem36  34012  dalem37  34013  dalem40  34016  dalem46  34022  dalem47  34023  dalem49  34025  dalem50  34026  dalem52  34028  dalem53  34029  dalem54  34030  dalem56  34032  dalem58  34034  dalem59  34035  dalem62  34038  paddval  34102  4atexlemex4  34377  4atexlemex6  34378  cdleme31sdnN  34693  cdlemefr44  34731  cdleme48fv  34805  cdlemeg49lebilem  34845  cdleme50eq  34847  rngunsnply  36762  ifpbiidcor  36838  frege129d  37074  axfrege54a  37175  iotaequ  37652  2uasban  37799  uunT1  38028  e2ebindVD  38170  e2ebindALT  38187  iunconALT  38194  disjinfi  38375  ioodvbdlimc1  38823  ioodvbdlimc2  38825  fourierdlem86  39085  fourierdlem94  39093  fourierdlem103  39102  fourierdlem104  39103  fourierdlem113  39112  hoidmvlelem1  39485  hoidmvlelem3  39487  hoidmvlelem4  39488  elfz0lmr  40367  nb3grpr  40610  frgr3v  41445  rngccatidALTV  41781  ringccatidALTV  41844