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

Theorem biid 227
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 19 . 2  |-  ( ph  ->  ph )
21, 1impbii 180 1  |-  ( ph  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  biidd  228  pm5.19  349  3anbi1i  1142  3anbi2i  1143  3anbi3i  1144  trujust  1309  tru  1312  trubitru  1340  falbifal  1343  hadcoma  1378  hadcomb  1379  hadnot  1383  cadcomb  1386  eqid  2283  abid2  2400  abid2f  2444  ceqsexg  2899  wecmpep  4385  ordon  4574  sorpss  6282  tz7.49c  6458  dford2  7321  infxpen  7642  isacn  7671  dfac5  7755  dfackm  7792  pwfseq  8286  axgroth5  8446  axgroth6  8450  supmul  9722  fsum2d  12234  rpnnen2  12504  isstruct  13158  oppccatid  13622  subccatid  13720  fuccatid  13843  setccatid  13916  catccatid  13934  xpccatid  13962  spwpr4  14340  opprsubg  15418  abvtriv  15606  lmodvscl  15644  opsrtos  16227  iscnp2  16969  cbvditg  19204  ditgsplit  19211  isosctrlem1  20118  lgsquad2  20599  eqid1  20840  grpoidinv  20875  stri  22837  hstri  22845  stcltrthi  22858  elxrge02  23116  nmo  23144  cvmliftlem11  23826  dfon2  24148  sltsolem1  24322  brpprod3b  24427  brapply  24477  brrestrict  24487  dfrdg4  24488  cgr3permute3  24670  cgr3permute1  24671  cgr3permute2  24672  cgr3permute4  24673  cgr3permute5  24674  colinearxfr  24698  brsegle  24731  vecval1b  25451  conttnf2  25562  cmptdst  25568  supnuf  25629  supexr  25631  rngunsnply  27378  symgsssg  27408  symgfisg  27409  iotaequ  27629  stoweidlem20  27769  frgra3v  28180  2uasban  28328  e2ebindVD  28688  e2ebindALT  28706  bnj1383  28864  bnj1386  28866  bnj153  28912  bnj543  28925  bnj544  28926  bnj546  28928  bnj605  28939  bnj579  28946  bnj600  28951  bnj601  28952  bnj852  28953  bnj893  28960  bnj906  28962  bnj917  28966  bnj938  28969  bnj944  28970  bnj998  28988  bnj1006  28991  bnj1029  28998  bnj1034  29000  bnj1124  29018  bnj1128  29020  bnj1127  29021  bnj1125  29022  bnj1147  29024  bnj1190  29038  bnj69  29040  bnj1204  29042  bnj1311  29054  bnj1318  29055  bnj1384  29062  bnj1408  29066  bnj1414  29067  bnj1415  29068  bnj1421  29072  bnj1423  29081  bnj1489  29086  bnj1493  29089  bnj60  29092  bnj1500  29098  bnj1522  29102  dalemeea  29852  dalem4  29854  dalem6  29857  dalem7  29858  dalem11  29863  dalem12  29864  dalem29  29890  dalem30  29891  dalem31N  29892  dalem32  29893  dalem33  29894  dalem34  29895  dalem35  29896  dalem36  29897  dalem37  29898  dalem40  29901  dalem46  29907  dalem47  29908  dalem49  29910  dalem50  29911  dalem52  29913  dalem53  29914  dalem54  29915  dalem56  29917  dalem58  29919  dalem59  29920  dalem62  29923  paddval  29987  4atexlemex4  30262  4atexlemex6  30263  cdleme31sdnN  30576  cdlemefr44  30614  cdleme48fv  30688  cdlemeg49lebilem  30728  cdleme50eq  30730
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator