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  4576  ordon  4765  sorpss  6529  tz7.49c  6705  dford2  7577  infxpen  7898  isacn  7927  dfac5  8011  dfackm  8048  pwfseq  8541  axgroth5  8701  axgroth6  8705  supmul  9978  fsum2d  12557  rpnnen2  12827  isstruct  13481  oppccatid  13947  subccatid  14045  fuccatid  14168  setccatid  14241  catccatid  14259  xpccatid  14287  spwpr4  14665  opprsubg  15743  abvtriv  15931  lmodvscl  15969  opsrtos  16548  iscnp2  17305  cbvditg  19743  ditgsplit  19750  lgsquad2  21146  nb3grapr  21464  eqid1  21763  grpoidinv  21798  stri  23762  hstri  23770  stcltrthi  23783  nmo  23975  elxrge02  24180  cvmliftlem11  24984  cbvprod  25243  fprod2d  25307  socnv  25390  dfon2  25421  sltsolem1  25625  brpprod3b  25734  brapply  25785  brrestrict  25796  dfrdg4  25797  cgr3permute3  25983  cgr3permute1  25984  cgr3permute2  25985  cgr3permute4  25986  cgr3permute5  25987  colinearxfr  26011  brsegle  26044  rngunsnply  27357  symgsssg  27387  symgfisg  27388  iotaequ  27608  frgra3v  28454  2uasban  28711  e2ebindVD  29086  e2ebindALT  29103  iunconALT  29110  bnj1383  29265  bnj1386  29267  bnj153  29313  bnj543  29326  bnj544  29327  bnj546  29329  bnj605  29340  bnj579  29347  bnj600  29352  bnj601  29353  bnj852  29354  bnj893  29361  bnj906  29363  bnj917  29367  bnj938  29370  bnj944  29371  bnj998  29389  bnj1006  29392  bnj1029  29399  bnj1034  29401  bnj1124  29419  bnj1128  29421  bnj1127  29422  bnj1125  29423  bnj1147  29425  bnj1190  29439  bnj69  29441  bnj1204  29443  bnj1311  29455  bnj1318  29456  bnj1384  29463  bnj1408  29467  bnj1414  29468  bnj1415  29469  bnj1421  29473  bnj1423  29482  bnj1489  29487  bnj1493  29490  bnj60  29493  bnj1500  29499  bnj1522  29503  dalemeea  30522  dalem4  30524  dalem6  30527  dalem7  30528  dalem11  30533  dalem12  30534  dalem29  30560  dalem30  30561  dalem31N  30562  dalem32  30563  dalem33  30564  dalem34  30565  dalem35  30566  dalem36  30567  dalem37  30568  dalem40  30571  dalem46  30577  dalem47  30578  dalem49  30580  dalem50  30581  dalem52  30583  dalem53  30584  dalem54  30585  dalem56  30587  dalem58  30589  dalem59  30590  dalem62  30593  paddval  30657  4atexlemex4  30932  4atexlemex6  30933  cdleme31sdnN  31246  cdlemefr44  31284  cdleme48fv  31358  cdlemeg49lebilem  31398  cdleme50eq  31400
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 179
  Copyright terms: Public domain W3C validator