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

Theorem 3bitr4i 268
Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3bitr4i.1  |-  ( ph  <->  ps )
3bitr4i.2  |-  ( ch  <->  ph )
3bitr4i.3  |-  ( th  <->  ps )
Assertion
Ref Expression
3bitr4i  |-  ( ch  <->  th )

Proof of Theorem 3bitr4i
StepHypRef Expression
1 3bitr4i.2 . 2  |-  ( ch  <->  ph )
2 3bitr4i.1 . . 3  |-  ( ph  <->  ps )
3 3bitr4i.3 . . 3  |-  ( th  <->  ps )
42, 3bitr4i 243 . 2  |-  ( ph  <->  th )
51, 4bitri 240 1  |-  ( ch  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  bibi2d  309  or4  514  pm4.14  561  pm4.71  611  pm5.32ri  619  an31  775  an4  797  orimdi  820  ordi  834  ordir  835  andir  838  dfbi3  863  orbidi  898  3anrot  939  3orrot  940  3ancoma  941  3orcoma  942  3orcomb  944  3ioran  950  3anbi123i  1140  3orbi123i  1141  an6  1261  3or6  1263  nancom  1290  xorcom  1298  xorass  1299  xorneg2  1303  xorbi12i  1305  hadbi  1377  hadcoma  1378  hadcomb  1379  cador  1381  cadan  1382  hadnot  1383  cadnot  1384  cadcoma  1385  cadcomb  1386  cad1  1388  nic-axALT  1429  nfbii  1559  19.26-3an  1585  19.43OLD  1596  cbvexvw  1689  19.32  1823  19.31  1824  19.42  1828  eeeanv  1867  equsex  1915  cbvex  1938  dfsb3  2009  sbor  2019  sban  2022  sbbi  2024  sb8e  2046  sb6  2051  pm11.07  2067  sbel2x  2077  sbex  2080  sb8eu  2174  sb8mo  2175  eu1  2177  sbmo  2186  cbvmo  2193  moanim  2212  eqcom  2298  abeq1  2402  cbvab  2414  clelab  2416  nfceqi  2428  sbabel  2458  ralbii2  2584  rexbii2  2585  r2alf  2591  r2exf  2592  r3al  2613  r19.30  2698  r19.32v  2699  r19.41  2705  r19.42v  2707  r19.43  2708  ralcomf  2711  rexcomf  2712  reean  2719  3reeanv  2721  2ralor  2722  rabid2  2730  rabbi  2731  reubiia  2738  rmobiia  2743  reu5  2766  rmo5  2769  cbvralf  2771  cbvrexf  2772  cbvreu  2775  cbvrmo  2776  vjust  2802  ceqsex3v  2839  ceqsex4v  2840  ceqsex8v  2842  eueq  2950  reu2  2966  reu6  2967  reu3  2968  rmo4  2971  2reu5  2986  cbvsbc  3032  sbccomlem  3074  rmo3  3091  csbabg  3155  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  eqss  3207  uniiunlem  3273  sspsstri  3291  ssequn1  3358  unss  3362  rexun  3368  ralunb  3369  elin3  3373  incom  3374  inass  3392  ssin  3404  nssinpss  3414  dfun2  3417  difin  3419  indi  3428  indifdir  3438  symdif2  3447  rabn0  3487  disj3  3512  ssdif0  3526  inssdif0  3534  ssundif  3550  dfif2  3580  snprc  3708  reusn  3713  difsnpss  3774  prss  3785  tpss  3795  pwpr  3839  eluni2  3847  elunirab  3856  uniun  3862  unissb  3873  elintrab  3890  ssintrab  3901  intun  3910  intpr  3911  iuncom  3927  iuncom4  3928  iunab  3964  ssiinf  3967  iunn0  3978  iinab  3979  iunin2  3982  iinun2  3984  iundif2  3985  iunun  3998  iunxun  3999  iunxiun  4000  sspwuni  4003  iinpw  4006  cbvdisj  4019  disjor  4023  brun  4085  brin  4086  brdif  4087  dftr2  4131  intexrab  4186  inuni  4189  ssext  4244  pweqb  4246  otth2  4265  opelopabsbOLD  4289  eqopab2b  4310  pwin  4313  pwun  4318  dflim2  4464  unisuc  4484  reusv2lem4  4554  reusv5OLD  4560  reusv7OLD  4562  sucexb  4616  sucelon  4624  dflim4  4655  xpiundi  4759  xpiundir  4760  poinxp  4769  soinxp  4770  frinxp  4771  seinxp  4772  weinxp  4773  inopab  4832  difopab  4833  raliunxp  4841  rexiunxp  4842  rexxpf  4847  iunxpf  4848  cnvco  4881  dmiun  4903  dmuni  4904  dm0rn0  4911  brres  4977  dmres  4992  cnvsym  5073  asymref  5075  codir  5079  qfto  5080  cnvopab  5099  cnvdif  5103  rniun  5107  dminss  5111  imainss  5112  dmsnn0  5154  cnvcnvsn  5166  resco  5193  imaco  5194  rnco  5195  coiun  5198  coass  5207  ressn  5227  cnviin  5228  cnvpo  5229  cnvso  5230  funcnv  5326  funcnv3  5327  fncnv  5330  fun11  5331  imadif  5343  fnres  5376  dfmpt3  5382  fnopabg  5383  fint  5436  fin  5437  fores  5476  dff1o3  5494  fun11iun  5509  f11o  5522  f1ompt  5698  fsn  5712  opabex3  5785  imaiun  5787  isocnv2  5844  isocnv3  5845  isores2  5846  isomin  5850  eqoprab2b  5922  difxp  6169  dfopab2  6190  dfoprab3s  6191  fmpt2x  6206  fparlem1  6234  fparlem2  6235  fsplit  6239  tpostpos  6270  dfsmo2  6380  brwitnlem  6522  oarec  6576  qsid  6741  mapval2  6813  map0e  6821  mapsncnv  6830  elixp2  6836  ixpin  6857  brsdom  6900  brdom2  6907  xpassen  6972  brsdom2  7001  unfilem1  7137  fiint  7149  dfsup2  7211  supmo  7219  rankc1  7558  cp  7577  isinfcard  7735  aceq1  7760  aceq2  7762  dfac5lem3  7768  dfac10b  7781  dfac12a  7790  dffin7-2  8040  dfacfin7  8041  fin1a2lem6  8047  iunfo  8177  konigthlem  8206  axgroth6  8466  axgroth3  8469  sstskm  8480  ltexprlem1  8676  gt0srpr  8716  ltpsrpr  8747  map2psrpr  8748  ltresr  8778  fimaxre3  9719  sup3  9727  supmul1  9735  elnn0z  10052  elznn0nn  10053  zmin  10328  xrnemnf  10476  xrnepnf  10477  elioomnf  10754  elxrge0  10763  elfzuzb  10808  elfz2nn0  10837  fzass4  10845  elfzo2  10894  elfzo3  10906  lbfzo0  10919  fzind2  10939  nn0opthlem1  11299  rexfiuz  11847  fsumcom2  12253  sinltx  12485  divalglem4  12611  divalglem10  12617  isprm2lem  12781  4sqlem12  13019  imasleval  13459  xpsfrnel  13481  xpscf  13484  isffth2  13806  ispos2  14098  ismhm  14433  nsgacs  14669  isgim  14742  oppgcntz  14853  efgrelexlemb  15075  pgpfac1  15331  pgpfac  15335  opprsubg  15434  opprunit  15459  isirred2  15499  opprirred  15500  drngprop  15539  opprdrng  15552  islss  15708  islbs  15845  isdomn2  16056  unocv  16596  iunocv  16597  istps2OLD  16675  isbasis2g  16702  tgval2  16710  ntreq0  16830  isclo2  16841  cmpcov2  17133  is1stc2  17184  1stcelcls  17203  llyi  17216  txuni2  17276  xkobval  17297  hausdiag  17355  isfbas2  17546  elfg  17582  fbasrn  17595  fmfnfmlem3  17667  isfcls  17720  alexsubALTlem2  17758  istmd  17773  istgp  17776  istrg  17862  istdrg  17864  istdrg2  17876  isms2  18012  isngp  18134  isngp2  18135  isngp3  18136  elii1  18449  iscph  18622  isbn  18776  pmltpc  18826  ovolfcl  18842  finiunmbl  18917  iundisj  18921  dyaddisj  18967  vitalilem1  18979  ellimc3  19245  ig1pval3  19576  plyun0  19595  plydivex  19693  aannenlem2  19725  ellogrn  19933  atandm  20188  atandm3  20190  atans2  20243  issubgo  20986  h2hlm  21576  issh  21803  chcon2i  22059  chcon1i  22060  chcon3i  22061  chnlei  22080  cmcm2i  22188  cmcm3i  22189  3oalem3  22259  pjdifnormii  22278  pjneli  22318  dfadj2  22481  cnvadj  22488  hhcno  22500  hhcnf  22501  eleigvec  22553  eleigvec2  22554  pjimai  22772  isst  22809  ishst  22810  cvnbtwn4  22885  chrelat4i  22969  ballotlemodife  23072  rabid2f  23151  cntnevol  23191  rmo3f  23194  rmo4fOLD  23195  mptfnf  23241  xrdifh  23288  cbvdisjf  23365  disjorf  23371  iundisjfi  23378  iundisjf  23380  eldifpr  23409  erdszelem1  23737  cvmliftlem15  23844  snmlval  23929  untuni  24070  dfso3  24089  dftr6  24178  coep  24179  coepr  24180  dffr5  24181  dfso2  24182  dfpo2  24183  cnvco1  24188  cnvco2  24189  eldm3  24190  dfdm5  24203  dfrn5  24204  wfrlem8  24334  wfrlem11  24337  tfrALTlem  24347  frrlem5c  24358  elno3  24380  nofulllem5  24431  elsymdif  24438  symdifass  24442  brsset  24500  idsset  24501  dfon3  24503  dfbigcup2  24510  dffix2  24516  dfom5b  24523  dffun10  24524  elfuns  24525  dfiota3  24533  fnimage  24539  brdomain  24543  brrange  24544  brimg  24547  brapply  24548  brrestrict  24559  tfrqfree  24561  altopelaltxp  24582  colinearalg  24610  axeuclid  24663  df3nandALT1  24907  imnand2  24910  supaddc  24995  itg2addnclem2  25004  fates  25058  evevifev  25117  uninqs  25142  elo  25144  restidsing  25179  dff1o6f  25195  cmpdom  25246  trooo  25497  isidlNEW  25549  cinvlem3  25933  cnvresimaOLD  26329  trer  26330  filnetlem4  26433  inixp  26502  prdstotbnd  26621  heibor1lem  26636  isrngohom  26699  isidl  26742  isfldidl2  26797  isdmn3  26802  moxfr  26855  fphpd  27002  f1omvdco3  27495  issdrg2  27609  pm10.541  27665  compab  27747  conss34  27748  r19.32  28048  rmoanim  28060  opabex3d  28190  bnj257  29048  bnj268  29050  bnj290  29051  bnj312  29053  bnj89  29063  bnj538  29085  bnj887  29111  bnj976  29125  bnj1019  29127  bnj1146  29139  bnj1385  29181  bnj110  29206  bnj121  29218  bnj130  29222  bnj153  29228  bnj543  29241  bnj580  29261  bnj607  29264  bnj849  29273  bnj882  29274  bnj916  29281  bnj985  29301  bnj1033  29315  bnj1083  29324  bnj1090  29325  bnj1128  29336  bnj1174  29349  bnj1228  29357  equsexNEW7  29467  cbvexwAUX7  29495  sborNEW7  29541  sbanNEW7  29544  sbbiNEW7  29545  sb8ewAUX7  29566  sb6NEW7  29569  sbel2xNEW7  29586  sbexNEW7  29589  dfsb3NEW7  29610  eeeanvOLD7  29658  cbvexOLD7  29680  sb8eOLD7  29711  pm11.07OLD7  29716  equsexv-x12  29735  pmapglbx  30580  lhpexle3  30823  cdleme25cv  31169  dicelval3  31992  diclspsn  32006  lcfls1c  32348
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