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

Theorem biid 227
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 19 . 2  |-  ( ph  ->  ph )
21, 1impbii 180 1  |-  ( ph  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  biidd  228  pm5.19  349  3anbi1i  1142  3anbi2i  1143  3anbi3i  1144  trujust  1309  tru  1312  trubitru  1340  falbifal  1343  hadcoma  1378  hadcomb  1379  hadnot  1383  cadcomb  1386  eqid  2296  abid2  2413  abid2f  2457  ceqsexg  2912  wecmpep  4401  ordon  4590  sorpss  6298  tz7.49c  6474  dford2  7337  infxpen  7658  isacn  7687  dfac5  7771  dfackm  7808  pwfseq  8302  axgroth5  8462  axgroth6  8466  supmul  9738  fsum2d  12250  rpnnen2  12520  isstruct  13174  oppccatid  13638  subccatid  13736  fuccatid  13859  setccatid  13932  catccatid  13950  xpccatid  13978  spwpr4  14356  opprsubg  15434  abvtriv  15622  lmodvscl  15660  opsrtos  16243  iscnp2  16985  cbvditg  19220  ditgsplit  19227  isosctrlem1  20134  lgsquad2  20615  eqid1  20856  grpoidinv  20891  stri  22853  hstri  22861  stcltrthi  22874  elxrge02  23132  nmo  23160  cvmliftlem11  23841  cbvcprod  24137  dfon2  24219  sltsolem1  24393  brpprod3b  24498  brapply  24548  brrestrict  24559  dfrdg4  24560  cgr3permute3  24742  cgr3permute1  24743  cgr3permute2  24744  cgr3permute4  24745  cgr3permute5  24746  colinearxfr  24770  brsegle  24803  vecval1b  25554  conttnf2  25665  cmptdst  25671  supnuf  25732  supexr  25734  rngunsnply  27481  symgsssg  27511  symgfisg  27512  iotaequ  27732  stoweidlem20  27872  nb3grapr  28289  frgra3v  28426  2uasban  28627  e2ebindVD  29004  e2ebindALT  29022  bnj1383  29180  bnj1386  29182  bnj153  29228  bnj543  29241  bnj544  29242  bnj546  29244  bnj605  29255  bnj579  29262  bnj600  29267  bnj601  29268  bnj852  29269  bnj893  29276  bnj906  29278  bnj917  29282  bnj938  29285  bnj944  29286  bnj998  29304  bnj1006  29307  bnj1029  29314  bnj1034  29316  bnj1124  29334  bnj1128  29336  bnj1127  29337  bnj1125  29338  bnj1147  29340  bnj1190  29354  bnj69  29356  bnj1204  29358  bnj1311  29370  bnj1318  29371  bnj1384  29378  bnj1408  29382  bnj1414  29383  bnj1415  29384  bnj1421  29388  bnj1423  29397  bnj1489  29402  bnj1493  29405  bnj60  29408  bnj1500  29414  bnj1522  29418  dalemeea  30474  dalem4  30476  dalem6  30479  dalem7  30480  dalem11  30485  dalem12  30486  dalem29  30512  dalem30  30513  dalem31N  30514  dalem32  30515  dalem33  30516  dalem34  30517  dalem35  30518  dalem36  30519  dalem37  30520  dalem40  30523  dalem46  30529  dalem47  30530  dalem49  30532  dalem50  30533  dalem52  30535  dalem53  30536  dalem54  30537  dalem56  30539  dalem58  30541  dalem59  30542  dalem62  30545  paddval  30609  4atexlemex4  30884  4atexlemex6  30885  cdleme31sdnN  31198  cdlemefr44  31236  cdleme48fv  31310  cdlemeg49lebilem  31350  cdleme50eq  31352
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 177
  Copyright terms: Public domain W3C validator