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

Theorem bitr2i 250
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 12-Mar-1993.)
Hypotheses
Ref Expression
bitr2i.1
bitr2i.2
Assertion
Ref Expression
bitr2i

Proof of Theorem bitr2i
StepHypRef Expression
1 bitr2i.1 . . 3
2 bitr2i.2 . . 3
31, 2bitri 249 . 2
43bicomi 202 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  3bitrri  272  3bitr2ri  274  3bitr4ri  278  nan  580  pm4.15  581  pm5.17  888  pm4.83  929  pm5.7  934  3or6  1310  nanim  1350  hadnot  1460  19.12vvv  1765  19.12vv  1986  2eu4OLD  2381  cvjust  2451  abbi  2588  abbiOLD  2589  necon1abii  2719  nabbi  2790  nrexralim  2911  r19.23v  2937  spc3gv  3199  ralxpxfr2d  3224  sbc8g  3335  ss2rab  3575  difdif  3629  ddif  3635  unass  3660  unss  3677  undi  3744  rabeq0  3807  disj  3867  ssindif0  3880  prneimg  4211  pwsnALT  4244  iinrab2  4393  unopab  4527  axrep5  4568  eqvinop  4736  pwssun  4791  dmun  5214  reldm0  5225  dmres  5299  imadmrn  5352  ssrnres  5450  dmsnn0  5478  coundi  5513  coundir  5514  cnvpo  5550  xpco  5552  fun11  5658  fununi  5659  isarep1  5672  fdmrn  5751  dffv2  5946  fsn  6069  fconstfvOLD  6134  eufnfv  6146  eloprabga  6389  funoprabg  6401  ralrnmpt2  6417  pwexb  6611  suceloni  6648  funcnvuni  6753  oprabrexex2  6790  fsplit  6905  dfer2  7331  euen1b  7606  xpsnen  7621  1sdom  7742  wemapsolem  7996  zfregcl  8041  epfrs  8183  rankbnd  8307  rankbnd2  8308  rankxplim2  8319  rankxplim3  8320  isinfcard  8494  dfac5lem2  8526  dfac5lem5  8529  kmlem14  8564  kmlem15  8565  kmlem16  8566  axdc2lem  8849  axcclem  8858  ac9  8884  ac9s  8894  nnunb  10816  xrrebnd  11398  elfznelfzo  11915  hashfun  12495  rexuz3  13181  imasaddfnlem  14925  isnsgrp  15915  pmtr3ncomlem1  16498  dprd2d2  17093  isnirred  17349  subsubrg2  17456  isdomn2  17948  mdetunilem7  19120  mdetunilem8  19121  maducoeval2  19142  tgval2  19457  0top  19485  ssntr  19559  uncmp  19903  opnfbas  20343  fbunfip  20370  hausflf2  20499  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALT  20551  metrest  21027  cfilucfil3OLD  21757  cfilucfil3  21758  ellimc3  22283  plyun0  22594  sinhalfpilem  22856  colinearalg  24213  axcontlem5  24271  nb3graprlem2  24452  2wlkeq  24707  clwwlkn2  24775  clwlkisclwwlklem2a4  24784  el2wlkonot  24869  el2spthonot  24870  shlesb1i  26304  pjneli  26641  cnlnssadj  26999  pjin2i  27112  cvnbtwn2  27206  cvnbtwn4  27208  mdsl1i  27240  mdsl2i  27241  hatomistici  27281  cdj3lem3b  27359  iuninc  27428  disjex  27451  disjexc  27452  fpwrelmapffslem  27555  fpwrelmapffs  27557  isarchi2  27729  ismntop  28004  coinfliprv  28421  ballotlem2  28427  ballotlemi1  28441  plymulx  28505  dfso2  29183  dfpo2  29184  19.12b  29234  soseq  29334  dfom5b  29562  elfuns  29565  tfrqfree  29601  dfint3  29602  hfext  29840  cnambfre  30063  itg2addnclem2  30067  itg2addnc  30069  trer  30134  heiborlem1  30307  eq0rabdioph  30710  rmspecnonsq  30843  rmxdioph  30958  wopprc  30972  islssfg2  31017  2sbc6g  31322  2sbc5g  31323  iotasbc2  31327  ralnex2  31435  2rexsb  32175  2rexrsb  32176  islindeps  33054  2sb5nd  33333  2sb5ndVD  33710  2sb5ndALT  33732  bnj168  33785  bnj153  33938  bnj605  33965  bnj607  33974  bnj986  34012  bnj1090  34035  bnj1128  34046  bj-abbi  34361  bj-axrep5  34378  lssat  34741  islshpat  34742  lcvnbtwn2  34752  pclfinclN  35674  lhpex2leN  35737  diclspsn  36921  dihmeetlem4preN  37033  dihmeetlem13N  37046  lcdlss  37346  mapd1o  37375  bj-ifid1g  37708  bj-ifan23  37729  dfhe3  37799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator