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  1144  3anbi2i  1145  3anbi3i  1146  trujust  1311  tru  1314  trubitru  1342  falbifal  1345  hadcoma  1380  hadcomb  1381  hadnot  1385  cadcomb  1388  eqid  2285  abid2  2402  abid2f  2446  ceqsexg  2901  wecmpep  4385  ordon  4574  sorpss  6244  tz7.49c  6454  dford2  7317  infxpen  7638  isacn  7667  dfac5  7751  dfackm  7788  pwfseq  8282  axgroth5  8442  axgroth6  8446  supmul  9718  fsum2d  12229  rpnnen2  12499  isstruct  13153  oppccatid  13617  subccatid  13715  fuccatid  13838  setccatid  13911  catccatid  13929  xpccatid  13957  spwpr4  14335  opprsubg  15413  abvtriv  15601  lmodvscl  15639  opsrtos  16222  iscnp2  16964  cbvditg  19199  ditgsplit  19206  isosctrlem1  20113  lgsquad2  20594  eqid1  20833  grpoidinv  20868  stri  22830  hstri  22838  stcltrthi  22851  cvmliftlem11  23231  dfon2  23550  axsltsolem1  23723  brpprod3b  23836  brapply  23885  brrestrict  23895  dfrdg4  23896  cgr3permute3  24078  cgr3permute1  24079  cgr3permute2  24080  cgr3permute4  24081  cgr3permute5  24082  colinearxfr  24106  brsegle  24139  vecval1b  24851  conttnf2  24962  cmptdst  24968  supnuf  25029  supexr  25031  rngunsnply  26778  symgsssg  26808  symgfisg  26809  iotaequ  27029  stoweidlem20  27169  2uasban  27600  e2ebindVD  27957  e2ebindALT  27975  bnj1383  28132  bnj1386  28134  bnj153  28180  bnj543  28193  bnj544  28194  bnj546  28196  bnj605  28207  bnj579  28214  bnj600  28219  bnj601  28220  bnj852  28221  bnj893  28228  bnj906  28230  bnj917  28234  bnj938  28237  bnj944  28238  bnj998  28256  bnj1006  28259  bnj1029  28266  bnj1034  28268  bnj1124  28286  bnj1128  28288  bnj1127  28289  bnj1125  28290  bnj1147  28292  bnj1190  28306  bnj69  28308  bnj1204  28310  bnj1311  28322  bnj1318  28323  bnj1384  28330  bnj1408  28334  bnj1414  28335  bnj1415  28336  bnj1421  28340  bnj1423  28349  bnj1489  28354  bnj1493  28357  bnj60  28360  bnj1500  28366  bnj1522  28370  dalemeea  29120  dalem4  29122  dalem6  29125  dalem7  29126  dalem11  29131  dalem12  29132  dalem29  29158  dalem30  29159  dalem31N  29160  dalem32  29161  dalem33  29162  dalem34  29163  dalem35  29164  dalem36  29165  dalem37  29166  dalem40  29169  dalem46  29175  dalem47  29176  dalem49  29178  dalem50  29179  dalem52  29181  dalem53  29182  dalem54  29183  dalem56  29185  dalem58  29187  dalem59  29188  dalem62  29191  paddval  29255  4atexlemex4  29530  4atexlemex6  29531  cdleme31sdnN  29844  cdlemefr44  29882  cdleme48fv  29956  cdlemeg49lebilem  29996  cdleme50eq  29998
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