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  2258  abid2  2375  abid2f  2419  ceqsexg  2874  wecmpep  4357  ordon  4546  sorpss  6216  tz7.49c  6426  dford2  7289  infxpen  7610  isacn  7639  dfac5  7723  dfackm  7760  pwfseq  8254  axgroth5  8414  axgroth6  8418  supmul  9690  fsum2d  12199  rpnnen2  12466  isstruct  13120  oppccatid  13584  subccatid  13682  fuccatid  13805  setccatid  13878  catccatid  13896  xpccatid  13924  spwpr4  14302  opprsubg  15380  abvtriv  15568  lmodvscl  15606  opsrtos  16189  iscnp2  16931  cbvditg  19166  ditgsplit  19173  isosctrlem1  20080  lgsquad2  20561  eqid1  20800  grpoidinv  20835  stri  22797  hstri  22805  stcltrthi  22818  cvmliftlem11  23198  dfon2  23517  axsltsolem1  23690  brpprod3b  23803  brapply  23852  brrestrict  23862  dfrdg4  23863  cgr3permute3  24045  cgr3permute1  24046  cgr3permute2  24047  cgr3permute4  24048  cgr3permute5  24049  colinearxfr  24073  brsegle  24106  vecval1b  24818  conttnf2  24929  cmptdst  24935  supnuf  24996  supexr  24998  rngunsnply  26745  symgsssg  26775  symgfisg  26776  iotaequ  26997  stoweidlem20  27104  2uasban  27381  e2ebindVD  27738  e2ebindALT  27756  bnj1383  27913  bnj1386  27915  bnj153  27961  bnj543  27974  bnj544  27975  bnj546  27977  bnj605  27988  bnj579  27995  bnj600  28000  bnj601  28001  bnj852  28002  bnj893  28009  bnj906  28011  bnj917  28015  bnj938  28018  bnj944  28019  bnj998  28037  bnj1006  28040  bnj1029  28047  bnj1034  28049  bnj1124  28067  bnj1128  28069  bnj1127  28070  bnj1125  28071  bnj1147  28073  bnj1190  28087  bnj69  28089  bnj1204  28091  bnj1311  28103  bnj1318  28104  bnj1384  28111  bnj1408  28115  bnj1414  28116  bnj1415  28117  bnj1421  28121  bnj1423  28130  bnj1489  28135  bnj1493  28138  bnj60  28141  bnj1500  28147  bnj1522  28151  dalemeea  29019  dalem4  29021  dalem6  29024  dalem7  29025  dalem11  29030  dalem12  29031  dalem29  29057  dalem30  29058  dalem31N  29059  dalem32  29060  dalem33  29061  dalem34  29062  dalem35  29063  dalem36  29064  dalem37  29065  dalem40  29068  dalem46  29074  dalem47  29075  dalem49  29077  dalem50  29078  dalem52  29080  dalem53  29081  dalem54  29082  dalem56  29084  dalem58  29086  dalem59  29087  dalem62  29090  paddval  29154  4atexlemex4  29429  4atexlemex6  29430  cdleme31sdnN  29743  cdlemefr44  29781  cdleme48fv  29855  cdlemeg49lebilem  29895  cdleme50eq  29897
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