MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biid 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  1324  tru  1327  trubitru  1356  falbifal  1359  hadcoma  1394  hadcomb  1395  hadnot  1399  cadcomb  1402  eqid  2404  abid2  2521  abid2f  2565  ceqsexg  3027  wecmpep  4534  ordon  4722  sorpss  6486  tz7.49c  6662  dford2  7531  infxpen  7852  isacn  7881  dfac5  7965  dfackm  8002  pwfseq  8495  axgroth5  8655  axgroth6  8659  supmul  9932  fsum2d  12510  rpnnen2  12780  isstruct  13434  oppccatid  13900  subccatid  13998  fuccatid  14121  setccatid  14194  catccatid  14212  xpccatid  14240  spwpr4  14618  opprsubg  15696  abvtriv  15884  lmodvscl  15922  opsrtos  16501  iscnp2  17257  cbvditg  19694  ditgsplit  19701  lgsquad2  21097  nb3grapr  21415  eqid1  21714  grpoidinv  21749  stri  23713  hstri  23721  stcltrthi  23734  nmo  23926  elxrge02  24131  cvmliftlem11  24935  cbvprod  25194  fprod2d  25258  dfon2  25362  sltsolem1  25536  brpprod3b  25641  brapply  25691  brrestrict  25702  dfrdg4  25703  cgr3permute3  25885  cgr3permute1  25886  cgr3permute2  25887  cgr3permute4  25888  cgr3permute5  25889  colinearxfr  25913  brsegle  25946  rngunsnply  27246  symgsssg  27276  symgfisg  27277  iotaequ  27497  frgra3v  28106  2uasban  28360  e2ebindVD  28733  e2ebindALT  28751  bnj1383  28909  bnj1386  28911  bnj153  28957  bnj543  28970  bnj544  28971  bnj546  28973  bnj605  28984  bnj579  28991  bnj600  28996  bnj601  28997  bnj852  28998  bnj893  29005  bnj906  29007  bnj917  29011  bnj938  29014  bnj944  29015  bnj998  29033  bnj1006  29036  bnj1029  29043  bnj1034  29045  bnj1124  29063  bnj1128  29065  bnj1127  29066  bnj1125  29067  bnj1147  29069  bnj1190  29083  bnj69  29085  bnj1204  29087  bnj1311  29099  bnj1318  29100  bnj1384  29107  bnj1408  29111  bnj1414  29112  bnj1415  29113  bnj1421  29117  bnj1423  29126  bnj1489  29131  bnj1493  29134  bnj60  29137  bnj1500  29143  bnj1522  29147  dalemeea  30145  dalem4  30147  dalem6  30150  dalem7  30151  dalem11  30156  dalem12  30157  dalem29  30183  dalem30  30184  dalem31N  30185  dalem32  30186  dalem33  30187  dalem34  30188  dalem35  30189  dalem36  30190  dalem37  30191  dalem40  30194  dalem46  30200  dalem47  30201  dalem49  30203  dalem50  30204  dalem52  30206  dalem53  30207  dalem54  30208  dalem56  30210  dalem58  30212  dalem59  30213  dalem62  30216  paddval  30280  4atexlemex4  30555  4atexlemex6  30556  cdleme31sdnN  30869  cdlemefr44  30907  cdleme48fv  30981  cdlemeg49lebilem  31021  cdleme50eq  31023
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