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

Theorem biid 228
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 20 . 2  |-  ( ph  ->  ph )
21, 1impbii 181 1  |-  ( ph  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  biidd  229  pm5.19  350  3anbi1i  1144  3anbi2i  1145  3anbi3i  1146  trujust  1327  tru  1330  trubitru  1359  falbifal  1362  hadcoma  1397  hadcomb  1398  hadnot  1402  cadcomb  1405  eqid  2435  abid2  2552  abid2f  2596  ceqsexg  3059  wecmpep  4566  ordon  4755  sorpss  6519  tz7.49c  6695  dford2  7567  infxpen  7888  isacn  7917  dfac5  8001  dfackm  8038  pwfseq  8531  axgroth5  8691  axgroth6  8695  supmul  9968  fsum2d  12547  rpnnen2  12817  isstruct  13471  oppccatid  13937  subccatid  14035  fuccatid  14158  setccatid  14231  catccatid  14249  xpccatid  14277  spwpr4  14655  opprsubg  15733  abvtriv  15921  lmodvscl  15959  opsrtos  16538  iscnp2  17295  cbvditg  19733  ditgsplit  19740  lgsquad2  21136  nb3grapr  21454  eqid1  21753  grpoidinv  21788  stri  23752  hstri  23760  stcltrthi  23773  nmo  23965  elxrge02  24170  cvmliftlem11  24974  cbvprod  25233  fprod2d  25297  socnv  25380  dfon2  25411  sltsolem1  25615  brpprod3b  25724  brapply  25775  brrestrict  25786  dfrdg4  25787  cgr3permute3  25973  cgr3permute1  25974  cgr3permute2  25975  cgr3permute4  25976  cgr3permute5  25977  colinearxfr  26001  brsegle  26034  rngunsnply  27336  symgsssg  27366  symgfisg  27367  iotaequ  27587  frgra3v  28319  2uasban  28576  e2ebindVD  28951  e2ebindALT  28968  iunconALT  28975  bnj1383  29130  bnj1386  29132  bnj153  29178  bnj543  29191  bnj544  29192  bnj546  29194  bnj605  29205  bnj579  29212  bnj600  29217  bnj601  29218  bnj852  29219  bnj893  29226  bnj906  29228  bnj917  29232  bnj938  29235  bnj944  29236  bnj998  29254  bnj1006  29257  bnj1029  29264  bnj1034  29266  bnj1124  29284  bnj1128  29286  bnj1127  29287  bnj1125  29288  bnj1147  29290  bnj1190  29304  bnj69  29306  bnj1204  29308  bnj1311  29320  bnj1318  29321  bnj1384  29328  bnj1408  29332  bnj1414  29333  bnj1415  29334  bnj1421  29338  bnj1423  29347  bnj1489  29352  bnj1493  29355  bnj60  29358  bnj1500  29364  bnj1522  29368  dalemeea  30387  dalem4  30389  dalem6  30392  dalem7  30393  dalem11  30398  dalem12  30399  dalem29  30425  dalem30  30426  dalem31N  30427  dalem32  30428  dalem33  30429  dalem34  30430  dalem35  30431  dalem36  30432  dalem37  30433  dalem40  30436  dalem46  30442  dalem47  30443  dalem49  30445  dalem50  30446  dalem52  30448  dalem53  30449  dalem54  30450  dalem56  30452  dalem58  30454  dalem59  30455  dalem62  30458  paddval  30522  4atexlemex4  30797  4atexlemex6  30798  cdleme31sdnN  31111  cdlemefr44  31149  cdleme48fv  31223  cdlemeg49lebilem  31263  cdleme50eq  31265
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 178
  Copyright terms: Public domain W3C validator