MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biid 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  1147  3anbi2i  1148  3anbi3i  1149  trujust  1314  tru  1317  tru2OLD  1318  trubitru  1346  falbifal  1349  hadcoma  1384  hadcomb  1385  hadnot  1389  cadcomb  1392  eqid  2256  abid2  2373  abid2f  2417  ceqsexg  2850  wecmpep  4322  ordon  4511  sorpss  6181  tz7.49c  6391  dford2  7254  infxpen  7575  isacn  7604  dfac5  7688  dfackm  7725  pwfseq  8219  axgroth5  8379  axgroth6  8383  supmul  9655  fsum2d  12164  rpnnen2  12431  isstruct  13085  oppccatid  13549  subccatid  13647  fuccatid  13770  setccatid  13843  catccatid  13861  xpccatid  13889  spwpr4  14267  opprsubg  15345  abvtriv  15533  lmodvscl  15571  opsrtos  16154  iscnp2  16896  cbvditg  19131  ditgsplit  19138  isosctrlem1  20045  lgsquad2  20526  eqid1  20765  grpoidinv  20800  stri  22762  hstri  22770  stcltrthi  22783  cvmliftlem11  23163  dfon2  23482  axsltsolem1  23655  brpprod3b  23768  brapply  23817  brrestrict  23827  dfrdg4  23828  cgr3permute3  24010  cgr3permute1  24011  cgr3permute2  24012  cgr3permute4  24013  cgr3permute5  24014  colinearxfr  24038  brsegle  24071  vecval1b  24783  conttnf2  24894  cmptdst  24900  supnuf  24961  supexr  24963  rngunsnply  26710  symgsssg  26740  symgfisg  26741  iotaequ  26962  stoweidlem20  27069  2uasban  27344  e2ebindVD  27701  e2ebindALT  27719  bnj1383  27876  bnj1386  27878  bnj153  27924  bnj543  27937  bnj544  27938  bnj546  27940  bnj605  27951  bnj579  27958  bnj600  27963  bnj601  27964  bnj852  27965  bnj893  27972  bnj906  27974  bnj917  27978  bnj938  27981  bnj944  27982  bnj998  28000  bnj1006  28003  bnj1029  28010  bnj1034  28012  bnj1124  28030  bnj1128  28032  bnj1127  28033  bnj1125  28034  bnj1147  28036  bnj1190  28050  bnj69  28052  bnj1204  28054  bnj1311  28066  bnj1318  28067  bnj1384  28074  bnj1408  28078  bnj1414  28079  bnj1415  28080  bnj1421  28084  bnj1423  28093  bnj1489  28098  bnj1493  28101  bnj60  28104  bnj1500  28110  bnj1522  28114  dalemeea  28982  dalem4  28984  dalem6  28987  dalem7  28988  dalem11  28993  dalem12  28994  dalem29  29020  dalem30  29021  dalem31N  29022  dalem32  29023  dalem33  29024  dalem34  29025  dalem35  29026  dalem36  29027  dalem37  29028  dalem40  29031  dalem46  29037  dalem47  29038  dalem49  29040  dalem50  29041  dalem52  29043  dalem53  29044  dalem54  29045  dalem56  29047  dalem58  29049  dalem59  29050  dalem62  29053  paddval  29117  4atexlemex4  29392  4atexlemex6  29393  cdleme31sdnN  29706  cdlemefr44  29744  cdleme48fv  29818  cdlemeg49lebilem  29858  cdleme50eq  29860
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator