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  28541  dalem4  28543  dalem6  28546  dalem7  28547  dalem11  28552  dalem12  28553  dalem29  28579  dalem30  28580  dalem31N  28581  dalem32  28582  dalem33  28583  dalem34  28584  dalem35  28585  dalem36  28586  dalem37  28587  dalem40  28590  dalem46  28596  dalem47  28597  dalem49  28599  dalem50  28600  dalem52  28602  dalem53  28603  dalem54  28604  dalem56  28606  dalem58  28608  dalem59  28609  dalem62  28612  paddval  28676  4atexlemex4  28951  4atexlemex6  28952  cdleme31sdnN  29265  cdlemefr44  29303  cdleme48fv  29377  cdlemeg49lebilem  29417  cdleme50eq  29419
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