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  2253  abid2  2366  abid2f  2410  ceqsexg  2836  wecmpep  4278  ordon  4465  sorpss  6134  tz7.49c  6344  dford2  7205  infxpen  7526  isacn  7555  dfac5  7639  dfackm  7676  pwfseq  8166  axgroth5  8326  axgroth6  8330  supmul  9602  fsum2d  12111  rpnnen2  12378  isstruct  13032  oppccatid  13466  subccatid  13564  fuccatid  13687  setccatid  13760  catccatid  13778  xpccatid  13806  spwpr4  14175  opprsubg  15253  abvtriv  15441  lmodvscl  15479  opsrtos  16059  iscnp2  16801  cbvditg  19036  ditgsplit  19043  isosctrlem1  19862  lgsquad2  20431  eqid1  20670  grpoidinv  20705  stri  22667  hstri  22675  stcltrthi  22688  cvmliftlem11  22997  dfon2  23316  axsltsolem1  23489  brpprod3b  23602  brapply  23651  brrestrict  23661  dfrdg4  23662  cgr3permute3  23844  cgr3permute1  23845  cgr3permute2  23846  cgr3permute4  23847  cgr3permute5  23848  colinearxfr  23872  brsegle  23905  vecval1b  24617  conttnf2  24728  cmptdst  24734  supnuf  24795  supexr  24797  rngunsnply  26544  symgsssg  26574  symgfisg  26575  iotaequ  26796  2uasban  27021  e2ebindVD  27378  e2ebindALT  27396  bnj1383  27553  bnj1386  27555  bnj153  27601  bnj543  27614  bnj544  27615  bnj546  27617  bnj605  27628  bnj579  27635  bnj600  27640  bnj601  27641  bnj852  27642  bnj893  27649  bnj906  27651  bnj917  27655  bnj938  27658  bnj944  27659  bnj998  27677  bnj1006  27680  bnj1029  27687  bnj1034  27689  bnj1124  27707  bnj1128  27709  bnj1127  27710  bnj1125  27711  bnj1147  27713  bnj1190  27727  bnj69  27729  bnj1204  27731  bnj1311  27743  bnj1318  27744  bnj1384  27751  bnj1408  27755  bnj1414  27756  bnj1415  27757  bnj1421  27761  bnj1423  27770  bnj1489  27775  bnj1493  27778  bnj60  27781  bnj1500  27787  bnj1522  27791  dalemeea  28653  dalem4  28655  dalem6  28658  dalem7  28659  dalem11  28664  dalem12  28665  dalem29  28691  dalem30  28692  dalem31N  28693  dalem32  28694  dalem33  28695  dalem34  28696  dalem35  28697  dalem36  28698  dalem37  28699  dalem40  28702  dalem46  28708  dalem47  28709  dalem49  28711  dalem50  28712  dalem52  28714  dalem53  28715  dalem54  28716  dalem56  28718  dalem58  28720  dalem59  28721  dalem62  28724  paddval  28788  4atexlemex4  29063  4atexlemex6  29064  cdleme31sdnN  29377  cdlemefr44  29415  cdleme48fv  29489  cdlemeg49lebilem  29529  cdleme50eq  29531
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