MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biid Structured version   Unicode version

Theorem biid 229
Description: Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
biid  |-  ( ph  <->  ph )

Proof of Theorem biid
StepHypRef Expression
1 id 21 . 2  |-  ( ph  ->  ph )
21, 1impbii 182 1  |-  ( ph  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 178
This theorem is referenced by:  biidd  230  pm5.19  351  3anbi1i  1145  3anbi2i  1146  3anbi3i  1147  trujust  1328  tru  1331  trubitru  1360  falbifal  1363  hadcoma  1398  hadcomb  1399  hadnot  1403  cadcomb  1406  eqid  2438  abid2  2555  abid2f  2599  ceqsexg  3069  wecmpep  4577  ordon  4766  sorpss  6530  tz7.49c  6706  dford2  7578  infxpen  7901  isacn  7930  dfac5  8014  dfackm  8051  pwfseq  8544  axgroth5  8704  axgroth6  8708  supmul  9981  fsum2d  12560  rpnnen2  12830  isstruct  13484  oppccatid  13950  subccatid  14048  fuccatid  14171  setccatid  14244  catccatid  14262  xpccatid  14290  spwpr4  14668  opprsubg  15746  abvtriv  15934  lmodvscl  15972  opsrtos  16551  iscnp2  17308  cbvditg  19746  ditgsplit  19753  lgsquad2  21149  nb3grapr  21467  eqid1  21766  grpoidinv  21801  stri  23765  hstri  23773  stcltrthi  23786  nmo  23978  elxrge02  24183  cvmliftlem11  24987  cbvprod  25246  fprod2d  25310  socnv  25393  dfon2  25424  sltsolem1  25628  brpprod3b  25737  brapply  25788  brrestrict  25799  dfrdg4  25800  cgr3permute3  25986  cgr3permute1  25987  cgr3permute2  25988  cgr3permute4  25989  cgr3permute5  25990  colinearxfr  26014  brsegle  26047  rngunsnply  27369  symgsssg  27399  symgfisg  27400  iotaequ  27620  frgra3v  28466  2uasban  28723  e2ebindVD  29098  e2ebindALT  29115  iunconALT  29122  bnj1383  29277  bnj1386  29279  bnj153  29325  bnj543  29338  bnj544  29339  bnj546  29341  bnj605  29352  bnj579  29359  bnj600  29364  bnj601  29365  bnj852  29366  bnj893  29373  bnj906  29375  bnj917  29379  bnj938  29382  bnj944  29383  bnj998  29401  bnj1006  29404  bnj1029  29411  bnj1034  29413  bnj1124  29431  bnj1128  29433  bnj1127  29434  bnj1125  29435  bnj1147  29437  bnj1190  29451  bnj69  29453  bnj1204  29455  bnj1311  29467  bnj1318  29468  bnj1384  29475  bnj1408  29479  bnj1414  29480  bnj1415  29481  bnj1421  29485  bnj1423  29494  bnj1489  29499  bnj1493  29502  bnj60  29505  bnj1500  29511  bnj1522  29515  dalemeea  30534  dalem4  30536  dalem6  30539  dalem7  30540  dalem11  30545  dalem12  30546  dalem29  30572  dalem30  30573  dalem31N  30574  dalem32  30575  dalem33  30576  dalem34  30577  dalem35  30578  dalem36  30579  dalem37  30580  dalem40  30583  dalem46  30589  dalem47  30590  dalem49  30592  dalem50  30593  dalem52  30595  dalem53  30596  dalem54  30597  dalem56  30599  dalem58  30601  dalem59  30602  dalem62  30605  paddval  30669  4atexlemex4  30944  4atexlemex6  30945  cdleme31sdnN  31258  cdlemefr44  31296  cdleme48fv  31370  cdlemeg49lebilem  31410  cdleme50eq  31412
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 179
  Copyright terms: Public domain W3C validator