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

Theorem 3bitr4i 269
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 244 . 2  |-  ( ph  <->  th )
51, 4bitri 241 1  |-  ( ch  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  bibi2d  310  or4  515  pm4.14  562  pm4.71  612  pm5.32ri  620  an31  776  an4  798  orimdi  821  ordi  835  ordir  836  andir  839  dfbi3  864  orbidi  899  3anrot  941  3orrot  942  3ancoma  943  3orcoma  944  3orcomb  946  3ioran  952  3anbi123i  1142  3orbi123i  1143  an6  1263  3or6  1265  nancom  1296  xorcom  1313  xorass  1314  xorneg2  1318  xorbi12i  1320  hadbi  1393  hadcoma  1394  hadcomb  1395  cador  1397  cadan  1398  hadnot  1399  cadnot  1400  cadcoma  1401  cadcomb  1402  cad1  1404  nic-axALT  1445  nfbii  1575  19.26-3an  1602  19.43OLD  1613  cbvexvw  1713  excom  1752  equsalhw  1856  19.32  1892  19.31  1893  19.42  1898  4exdistr  1930  eeeanv  1934  eeeanvOLD  1935  equsal  1966  equsexOLD  1970  cbvex  2038  dfsb3  2105  sbor  2115  sban  2118  sbbi  2120  sb6  2148  pm11.07OLD  2165  sbel2x  2175  sbex  2178  sb8eu  2272  sb8mo  2273  eu1  2275  sbmo  2284  cbvmo  2291  moanim  2310  eqcom  2406  abeq1  2510  cbvab  2522  clelab  2524  nfceqi  2536  sbabel  2566  ralbii2  2694  rexbii2  2695  r2alf  2701  r2exf  2702  r3al  2723  r19.30  2813  r19.32v  2814  r19.41  2820  r19.42v  2822  r19.43  2823  ralcomf  2826  rexcomf  2827  reean  2834  3reeanv  2836  2ralor  2837  rabid2  2845  rabbi  2846  reubiia  2853  rmobiia  2858  reu5  2881  rmo5  2884  cbvralf  2886  cbvrexf  2887  cbvreu  2890  cbvrmo  2891  vjust  2917  ceqsex3v  2954  ceqsex4v  2955  ceqsex8v  2957  eueq  3066  reu2  3082  reu6  3083  reu3  3084  rmo4  3087  2reu5  3102  cbvsbc  3149  sbccomlem  3191  rmo3  3208  csbabg  3270  cbvralcsf  3271  cbvrexcsf  3272  cbvreucsf  3273  eqss  3323  uniiunlem  3391  sspsstri  3409  ssequn1  3477  unss  3481  rexun  3487  ralunb  3488  elin3  3492  incom  3493  inass  3511  ssin  3523  nssinpss  3533  dfun2  3536  difin  3538  indi  3547  indifdir  3557  symdif2  3567  rabn0  3607  disj3  3632  ssdif0  3646  inssdif0  3655  ssundif  3671  dfif2  3701  snprc  3831  reusn  3837  difsnpss  3901  prss  3912  tpss  3924  pwpr  3971  eluni2  3979  elunirab  3988  uniun  3994  unissb  4005  elintrab  4022  ssintrab  4033  intun  4042  intpr  4043  iuncom  4059  iuncom4  4060  iunab  4097  ssiinf  4100  iunn0  4111  iinab  4112  iunin2  4115  iinun2  4117  iundif2  4118  iunun  4131  iunxun  4132  iunxiun  4133  sspwuni  4136  iinpw  4139  cbvdisj  4152  disjor  4156  brun  4218  brin  4219  brdif  4220  dftr2  4264  intexrab  4319  inuni  4322  ssext  4378  pweqb  4380  otth2  4399  opelopabsbOLD  4423  eqopab2b  4444  pwin  4447  pwun  4451  dflim2  4597  unisuc  4617  reusv5OLD  4692  reusv7OLD  4694  sucexb  4748  sucelon  4756  dflim4  4787  xpiundi  4891  xpiundir  4892  poinxp  4900  soinxp  4901  frinxp  4902  seinxp  4903  weinxp  4904  inopab  4964  difopab  4965  raliunxp  4973  rexiunxp  4974  rexxpf  4979  iunxpf  4980  cnvco  5015  dmiun  5037  dmuni  5038  dm0rn0  5045  brres  5111  dmres  5126  cnvsym  5207  asymref  5209  codir  5213  qfto  5214  cnvopab  5233  cnvdif  5237  rniun  5241  dminss  5245  imainss  5246  dmsnn0  5294  cnvcnvsn  5306  resco  5333  imaco  5334  rnco  5335  coiun  5338  coass  5347  ressn  5367  cnviin  5368  cnvpo  5369  cnvso  5370  xpco  5373  funcnv  5470  funcnv3  5471  fncnv  5474  fun11  5475  imadif  5487  fnres  5520  dfmpt3  5526  fnopabg  5527  fint  5581  fin  5582  fores  5621  dff1o3  5639  fun11iun  5654  f11o  5667  f1ompt  5850  fsn  5865  opabex3d  5948  opabex3  5949  imaiun  5951  isocnv2  6010  isocnv3  6011  isores2  6012  isomin  6016  eqoprab2b  6091  difxp  6339  dfopab2  6360  dfoprab3s  6361  fmpt2x  6376  fparlem1  6405  fparlem2  6406  fsplit  6410  tpostpos  6458  dfsmo2  6568  brwitnlem  6710  oarec  6764  qsid  6929  uniinqs  6943  mapval2  7002  map0e  7010  mapsncnv  7019  elixp2  7025  ixpin  7046  brsdom  7089  brdom2  7096  xpassen  7161  brsdom2  7190  unfilem1  7330  fiint  7342  dfsup2  7405  supmo  7413  rankc1  7752  cp  7771  isinfcard  7929  aceq1  7954  aceq2  7956  dfac5lem3  7962  dfac10b  7975  dfac12a  7984  dffin7-2  8234  dfacfin7  8235  fin1a2lem6  8241  iunfo  8370  konigthlem  8399  axgroth6  8659  axgroth3  8662  sstskm  8673  ltexprlem1  8869  gt0srpr  8909  ltpsrpr  8940  map2psrpr  8941  ltresr  8971  fimaxre3  9913  sup3  9921  supmul1  9929  elnn0z  10250  elznn0nn  10251  zmin  10526  xrnemnf  10674  xrnepnf  10675  elioomnf  10955  elxrge0  10964  elfzuzb  11009  elfz2nn0  11038  fzass4  11046  elfzo2  11098  elfzo3  11110  lbfzo0  11125  fzind2  11153  nn0opthlem1  11516  rexfiuz  12106  fsumcom2  12513  sinltx  12745  divalglem4  12871  divalglem10  12877  isprm2lem  13041  4sqlem12  13279  imasleval  13721  xpsfrnel  13743  xpscf  13746  isssc  13975  isffth2  14068  ispos2  14360  ismhm  14695  nsgacs  14931  isgim  15004  oppgcntz  15115  efgrelexlemb  15337  pgpfac1  15593  pgpfac  15597  opprsubg  15696  opprunit  15721  isirred2  15761  opprirred  15762  drngprop  15801  opprdrng  15814  islss  15966  islbs  16103  isdomn2  16314  unocv  16862  iunocv  16863  istps2OLD  16941  isbasis2g  16968  tgval2  16976  ntreq0  17096  isclo2  17107  cmpcov2  17407  is1stc2  17458  1stcelcls  17477  llyi  17490  txuni2  17550  xkobval  17571  hausdiag  17630  isfbas2  17820  elfg  17856  fbasrn  17869  fmfnfmlem3  17941  isfcls  17994  alexsubALTlem2  18032  istmd  18057  istgp  18060  istrg  18146  istdrg  18148  istdrg2  18160  isms2  18433  metuel2  18562  restmetu  18570  isngp  18596  isngp2  18597  isngp3  18598  elii1  18913  iscph  19086  isbn  19244  pmltpc  19300  ovolfcl  19316  finiunmbl  19391  iundisj  19395  dyaddisj  19441  vitalilem1  19453  ellimc3  19719  ig1pval3  20050  plyun0  20069  plydivex  20167  aannenlem2  20199  ellogrn  20410  atandm  20669  atandm3  20671  atans2  20724  issubgo  21844  h2hlm  22436  issh  22663  chcon2i  22919  chcon1i  22920  chcon3i  22921  chnlei  22940  cmcm2i  23048  cmcm3i  23049  3oalem3  23119  pjdifnormii  23138  pjneli  23178  dfadj2  23341  cnvadj  23348  hhcno  23360  hhcnf  23361  eleigvec  23413  eleigvec2  23414  pjimai  23632  isst  23669  ishst  23670  cvnbtwn4  23745  chrelat4i  23829  rabid2f  23920  rmo3f  23935  rmo4fOLD  23936  cbvdisjf  23968  disjorf  23974  iundisjf  23982  disjexc  23986  mptfnf  24026  xrdifh  24096  iundisjfi  24105  xrnarchi  24207  eldifpr  24345  cntnevol  24535  ballotlemodife  24708  erdszelem1  24830  cvmliftlem15  24938  snmlval  24971  untuni  25111  dfso3  25130  prodmo  25215  fprodcom2  25261  dftr6  25321  coep  25322  coepr  25323  dffr5  25324  dfso2  25325  dfpo2  25326  cnvco1  25331  cnvco2  25332  eldm3  25333  dfdm5  25346  dfrn5  25347  wfrlem8  25477  wfrlem11  25480  tfrALTlem  25490  frrlem5c  25501  elno3  25523  nofulllem5  25574  elsymdif  25581  symdifass  25585  brsset  25643  idsset  25644  dfon3  25646  dfbigcup2  25653  dffix2  25659  dfom5b  25666  dffun10  25667  elfuns  25668  dfiota3  25676  fnimage  25682  brdomain  25686  brrange  25687  brimg  25690  brapply  25691  funpartlem  25695  brrestrict  25702  tfrqfree  25704  altopelaltxp  25725  colinearalg  25753  axeuclid  25806  df3nandALT1  26050  imnand2  26053  supaddc  26137  ismblfin  26146  mbfposadd  26153  itg2addnclem2  26156  trer  26209  filnetlem4  26300  inixp  26320  prdstotbnd  26393  heibor1lem  26408  isrngohom  26471  isidl  26514  isfldidl2  26569  isdmn3  26574  moxfr  26623  fphpd  26767  f1omvdco3  27260  issdrg2  27374  pm10.541  27430  compab  27511  conss34  27512  r19.32  27812  rmoanim  27824  usgra2pth0  28042  usgreg2spot  28170  bnj257  28777  bnj268  28779  bnj290  28780  bnj312  28782  bnj89  28792  bnj538  28814  bnj887  28840  bnj976  28854  bnj1019  28856  bnj1146  28868  bnj1385  28910  bnj110  28935  bnj121  28947  bnj130  28951  bnj153  28957  bnj543  28970  bnj580  28990  bnj607  28993  bnj849  29002  bnj882  29003  bnj916  29010  bnj985  29030  bnj1033  29044  bnj1083  29053  bnj1090  29054  bnj1128  29065  bnj1174  29078  bnj1228  29086  equsexNEW7  29196  cbvexwAUX7  29224  sborNEW7  29270  sbanNEW7  29273  sbbiNEW7  29274  sb8ewAUX7  29295  sb6NEW7  29298  sbel2xNEW7  29315  sbexNEW7  29318  dfsb3NEW7  29340  eeeanvOLD7  29388  cbvexOLD7  29410  sb8eOLD7  29441  pmapglbx  30251  lhpexle3  30494  cdleme25cv  30840  dicelval3  31663  diclspsn  31677  lcfls1c  32019
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 178
  Copyright terms: Public domain W3C validator