Theorem 3bitr4i 303

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, 3-Jan-1993.)

Hypotheses

Ref	Expression
3bitr4i.1	⊢ (𝜑 ↔ 𝜓)
3bitr4i.2	⊢ (𝜒 ↔ 𝜑)
3bitr4i.3	⊢ (𝜃 ↔ 𝜓)

Assertion

Ref	Expression
3bitr4i	⊢ (𝜒 ↔ 𝜃)

Proof of Theorem 3bitr4i

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 ⊢ (𝜒 ↔ 𝜑)
2		3bitr4i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		3bitr4i.3	. . 3 ⊢ (𝜃 ↔ 𝜓)
4	2, 3	bitr4i 278	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitri 275	1 ⊢ (𝜒 ↔ 𝜃)

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  bibi2d  342  pm4.71  557  pm5.32ri  575  an31  648  pm4.14  806  or4  926  orimdi  930  orbidi  954  ordi  1007  ordir  1008  andir  1010  dfbi3  1049  dfifp7  1069  ifpdfbi  1070  ifpn  1073  3orrot  1091  3orcoma  1092  3ioran  1105  3ianor  1106  3anbi123i  1155  3orbi123i  1156  3jaob  1428  an6  1447  3or6  1449  an3andi  1484  an33rean  1485  nancom  1496  xorass  1515  anxordi  1526  norass  1537  hadbi  1598  hadcoma  1599  hadcomb  1600  hadnot  1602  cador  1608  cadan  1609  cadcoma  1612  cadnot  1615  nic-axALT  1674  19.26-3an  1872  19.43OLD  1883  19.32v  1940  19.31v  1941  19.42v  1953  4exdistr  1961  cbvexvw  2037  exexw  2052  sb3an  2082  sbcom4  2090  sbbiiev  2093  excom  2163  sbal  2170  19.32  2234  19.31  2235  19.42  2237  equsalv  2268  sbex  2281  sbrim  2304  sbor  2306  sbbi  2307  sbnfOLD  2312  cbvex2v  2342  eeeanv  2348  sbnf2  2356  cbvsbvf  2361  cbvex2  2410  equsal  2415  dfsb3  2492  mo4  2559  eu6  2567  eubii  2578  dfeu  2588  sb8eulem  2591  sb8mo  2594  cbvmovw  2595  cbvmow  2596  cbveuvw  2598  cbveuw  2599  cbveuALT  2601  eu1  2603  sbmo  2607  cbvabv  2799  cbvabw  2800  cbvab  2801  eqabcb  2869  nfceqi  2888  ralbii2  3071  rexbii2  3072  r19.26-3  3092  r19.43  3101  r2allem  3121  r19.42v  3167  r19.32v  3168  reeanlem  3206  3reeanv  3208  cbvralvw  3213  cbvrexvw  3214  ralcom  3263  ralcomf  3274  rexcomf  3275  cbvralfw  3276  cbvralsvw  3287  cbvralf  3331  cbvrexf  3332  reu5  3353  rmobiia  3357  reubiia  3358  rmoanidOLD  3363  reuanidOLD  3364  rmo5  3371  cbvrmovw  3374  cbvreuvw  3375  cbvrmow  3378  cbvreuw  3379  cbvreu  3394  cbvrmo  3395  rabid2f  3434  abv  3456  abvALT  3457  ceqsal  3482  ceqsalv  3484  cgsex4gOLD  3492  ceqsex3v  3500  ceqsex4v  3501  ceqsex8v  3503  reurab  3669  eueq  3676  reu2  3693  reu6  3694  reu3  3695  rmo4  3698  rmo3f  3702  2reu5  3726  cbvsbcw  3783  cbvsbcvw  3784  cbvsbc  3785  sbc3an  3815  sbccomlemOLD  3830  rmo3  3849  rmoanim  3854  rmoanimALT  3855  cbvralcsf  3901  cbvrexcsf  3902  cbvreucsf  3903  eqss  3959  uniiunlem  4046  sspsstri  4064  compleq  4111  ssequn1  4145  unss  4149  rexun  4155  ralunb  4156  elin3  4165  inass  4187  ssin  4198  elsymdif  4217  nssinpss  4226  dfun2  4229  difin  4231  indi  4243  indifdi  4253  difin2  4260  ssdif0  4325  inn0f  4330  inssdif0  4333  ab0  4339  abn0  4344  rabeq0w  4346  rabeq0  4347  disj  4409  disj3  4413  ssundif  4447  ralidmw  4467  dfif2  4486  eldifpr  4618  rexdifpr  4619  rexsns  4631  snprc  4677  reusn  4687  difsnpss  4767  tpss  4797  pwpr  4861  eluni2  4871  elunirab  4882  uniun  4890  unissb  4899  unissbOLD  4900  elintrab  4920  ssintrab  4931  intun  4940  iuncom  4959  iuncom4  4960  iunab  5010  ssiinf  5013  iunn0  5026  iinab  5027  iunin2  5030  iinun2  5032  iundif2  5033  iunun  5052  iunxun  5053  iunxiun  5056  sspwuni  5059  iinpw  5065  cbvdisj  5079  cbvdisjv  5080  disjor  5084  brun  5153  brin  5154  brdif  5155  dftr2  5211  dftr5  5213  intexrab  5297  inuni  5300  ssext  5409  pweqb  5411  otth2  5438  otthne  5441  propeqop  5462  vopelopabsb  5484  eqopab2bw  5503  eqopab2b  5507  pwin  5522  pwun  5524  dffr6  5587  elxp2  5655  otelxp  5675  xpiundi  5702  xpiundir  5703  poinxp  5712  soinxp  5713  frinxp  5714  seinxp  5715  weinxp  5716  inopab  5783  difopab  5784  inxp  5785  raliunxp  5793  rexiunxp  5794  rexxpf  5801  iunxpf  5802  cnvco  5839  dmiun  5867  dmuni  5868  dm0rn0  5878  dmres  5972  restidsing  6013  cnvsymOLDOLD  6075  asymref  6077  codir  6081  qfto  6082  cnvopab  6098  cnvopabOLD  6099  cnvdif  6104  rniun  6108  dminss  6114  imainss  6115  difxp  6125  xpdifid  6129  dmsnn0  6168  cnvcnvsn  6180  cnvresima  6191  resco  6211  imaco  6212  rnco  6213  coiun  6217  coass  6226  ressn  6246  cnviin  6247  cnvpo  6248  cnvso  6249  xpco  6250  opreu2reurex  6255  dfpo2  6257  imaindm  6260  dflim2  6378  funcnv  6569  funcnv3  6570  fncnv  6573  fun11  6574  imadif  6584  fnres  6627  dfmpt3  6634  mptfnf  6635  fnopabg  6637  fint  6721  fin  6722  fores  6764  dff1o3  6788  f1ompt  7065  fsn  7089  imaiun  7201  isocnv2  7288  isocnv3  7289  isores2  7290  isomin  7294  eqoprab2bw  7439  eqoprab2b  7440  elpwpwel  7723  sucexb  7760  onsucb  7772  dflim4  7804  fiun  7901  f1iun  7902  f11o  7905  opabex3d  7923  opabex3rd  7924  opabex3  7925  dfopab2  8010  dfoprab3s  8011  fmpox  8025  fparlem1  8068  fparlem2  8069  tpostpos  8202  frrlem9  8250  dfsmo2  8293  brwitnlem  8448  oarec  8503  naddasslem1  8635  naddasslem2  8636  qsid  8731  uniinqs  8747  mapval2  8822  mapsncnv  8843  elixp2  8851  ixpin  8873  brsdom  8923  brdom2  8930  xpassen  9012  brsdom2  9042  dif1enOLD  9103  unfilem1  9230  fiint  9253  fiintOLD  9254  dfsup2  9371  supmo  9379  eqinf  9412  infmo  9424  brttrcl2  9643  rankc1  9799  cp  9820  isinfcard  10021  aceq1  10046  aceq2  10048  dfac5lem3  10054  dfac10b  10069  dfac12a  10078  dffin7-2  10327  dfacfin7  10328  fin1a2lem6  10334  iunfo  10468  konigthlem  10497  axgroth6  10757  axgroth3  10760  sstskm  10771  ltexprlem1  10965  gt0srpr  11007  ltpsrpr  11038  map2psrpr  11039  ltresr  11069  fimaxre3  12105  sup3  12116  supaddc  12126  supmul1  12128  elnn0z  12518  elznn0nn  12519  zmin  12879  xrnemnf  13053  xrnepnf  13054  dfrp2  13331  elioomnf  13381  elxrge0  13394  elfzuzb  13455  fzass4  13499  elfz2nn0  13555  elfzo2  13599  elfzo3  13613  lbfzo0  13636  fzo1lb  13650  fzind2  13722  nn0opthlem1  14209  hashgt23el  14365  cotr2g  14918  rexfiuz  15290  fsumcom2  15716  prodmo  15878  fprodcom2  15926  sinltx  16133  divalglem4  16342  divalglem10  16348  4sqlem12  16903  imasleval  17480  xpsfrnel  17501  xpscf  17504  isssc  17758  isffth2  17856  ispos2  18252  issubmgm  18605  ismhm  18688  issubmndb  18708  nsgacs  19070  isgim  19170  oppgcntz  19272  f1omvdco3  19355  pmtrprfvalrn  19394  efgrelexlemb  19656  pgpfac1  19988  pgpfac  19992  issrg  20073  opprsubg  20237  opprunit  20262  isirred2  20306  opprirred  20307  opprnzrb  20406  isdomn2OLD  20597  opprdomnb  20602  isdomn4r  20604  drngprop  20629  opprdrng  20649  issdrg2  20680  islss  20816  islbs  20959  unocv  21565  iunocv  21566  isbasis2g  22811  tgval2  22819  ntreq0  22940  isclo2  22951  cmpcov2  23253  is1stc2  23305  1stcelcls  23324  llyi  23337  unisngl  23390  txuni2  23428  xkobval  23449  hausdiag  23508  isfbas2  23698  elfg  23734  fbasrn  23747  fmfnfmlem3  23819  isfcls  23872  alexsubALTlem2  23911  istmd  23937  istgp  23940  istrg  24027  istdrg  24029  istdrg2  24041  isms2  24314  metuel2  24429  restmetu  24434  isngp  24460  isngp2  24461  isngp3  24462  elii1  24807  isncvsngp  25025  iscph  25046  isbn  25214  pmltpc  25327  ovolfcl  25343  finiunmbl  25421  iundisj  25425  dyaddisj  25473  vitalilem1  25485  ellimc3  25756  ig1pval3  26059  plyun0  26078  plydivex  26181  aannenlem2  26213  ellogrn  26444  atandm  26762  atandm3  26764  atans2  26817  elno3  27543  conway  27687  eqscut2  27694  madeval2  27737  tgjustf  28376  colinearalg  28813  axeuclid  28866  nbgrsym  29266  upgrtrls  29603  upgristrl  29604  dfpth2  29632  usgr2pth0  29668  iswwlks  29739  isclwwlk  29886  clwwlkneq0  29931  h2hlm  30882  issh  31110  chcon2i  31366  chcon1i  31367  chcon3i  31368  chnlei  31387  cmcm2i  31495  cmcm3i  31496  3oalem3  31566  pjdifnormii  31585  pjneli  31625  dfadj2  31787  cnvadj  31794  hhcno  31806  hhcnf  31807  eleigvec  31859  eleigvec2  31860  pjimai  32078  isst  32115  ishst  32116  cvnbtwn4  32191  chrelat4i  32275  2reucom  32382  reuxfrdf  32393  difrab2  32400  inpr0  32434  iunin1f  32459  disjnf  32472  cbvdisjf  32473  disjorf  32481  iundisjf  32491  disjexc  32495  xrdifh  32676  iundisjfi  32692  hashxpe  32705  pmtrprfv2  33018  xrnarchi  33111  isunit2  33164  isorng  33250  prmidl0  33394  opprnsg  33428  ccfldextdgrr  33640  cmpcref  33813  ordtconnlem1  33887  isrrext  33963  cntnevol  34191  ddemeas  34199  omssubaddlem  34263  omssubadd  34264  eulerpartleme  34327  eulerpartlemv  34328  eulerpartlemt0  34333  eulerpartlemgvv  34340  eulerpartlemn  34345  ballotlem2  34453  ballotlemodife  34462  oddprm2  34619  bnj257  34670  bnj268  34672  bnj290  34673  bnj312  34675  bnj89  34684  bnj887  34728  bnj976  34740  bnj1019  34742  bnj1146  34754  bnj1385  34795  bnj110  34821  bnj121  34833  bnj130  34837  bnj153  34843  bnj543  34856  bnj580  34876  bnj607  34879  bnj849  34888  bnj882  34889  bnj916  34896  bnj985v  34916  bnj985  34917  bnj1033  34932  bnj1083  34941  bnj1090  34942  bnj1128  34953  bnj1174  34966  bnj1228  34974  onvf1odlem1  35063  erdszelem1  35151  cvmliftlem15  35258  snmlval  35291  satfvsuclem2  35320  satfdm  35329  elmpst  35496  mpstrcl  35501  orbi2iALT  35645  untuni  35669  dfso3  35680  xpab  35686  dftr6  35711  coep  35712  coepr  35713  dffr5  35714  dfso2  35715  cnvco1  35719  cnvco2  35720  eldm3  35721  dfdm5  35733  dfrn5  35734  brsset  35850  idsset  35851  dfon3  35853  dfbigcup2  35860  dfom5b  35873  dffun10  35875  dfiota3  35884  fnimage  35890  brdomain  35894  brrange  35895  brimg  35898  brapply  35899  brcup  35900  brcap  35901  brsuccf  35902  funpartlem  35903  brrestrict  35910  dfrecs2  35911  brub  35915  altopelaltxp  35937  rmoeqi  36148  rmoeqbii  36149  reueqi  36150  reueqbii  36151  sbceqbii  36152  disjeq1i  36153  cbvralvw2  36187  cbvrexvw2  36188  cbvrmovw2  36189  cbvreuvw2  36190  cbvsbcvw2  36191  cbvdisjvw2  36196  trer  36277  filnetlem4  36342  df3nandALT1  36360  imnand2  36363  bj-dfbi5  36535  bj-bixor  36552  bj-nnfnt  36701  bj-csbsnlem  36864  bj-rcleqf  36986  bj-sscon  36990  bj-pw0ALT  37010  bj-restpw  37053  bj-opelidb1  37114  bj-imdiridlem  37146  bj-imdirco  37151  wl-df3xor2  37430  wl-3xorrot  37438  wl-3xorcoma  37439  wl-3xornot  37442  wl-df2-3mintru2  37446  wl-df3-3mintru2  37447  wl-df4-3mintru2  37448  wl-equsalvw  37499  wl-sb9v  37510  iundif1  37561  poimirlem25  37612  poimirlem26  37613  poimirlem30  37617  ismblfin  37628  mbfposadd  37634  itg2addnclem2  37639  ftc1anc  37668  inixp  37695  prdstotbnd  37761  heibor1lem  37776  isrngohom  37932  isidl  37981  isfldidl2  38036  isdmn3  38041  sbccom2lem  38091  triantru3  38191  vvdifopab  38222  brres2  38230  eldmqsres  38248  inxpss  38272  ref5  38274  n0el2  38290  trcoss2  38448  dfeqvrel2  38554  dfeqvrel3  38555  redundeq1  38593  redundpbi1  38595  refrelredund4  38599  funALTVfun  38663  dfeldisj3  38684  dfeldisj5  38686  pet0  38780  petid  38782  petidres  38784  petinidres  38786  petxrnidres  38788  mpet  38804  petincnvepres  38814  pet  38816  pmapglbx  39736  lhpexle3  39979  cdleme25cv  40325  dicelval3  41147  diclspsn  41161  lcfls1c  41503  sn-axrep5v  42177  sn-iotalem  42182  psspwb  42189  redvmptabs  42321  eu6w  42637  moxfr  42653  fphpd  42777  uniel  43179  dflim6  43226  onsucf1olem  43232  dflim7  43235  omge2  43260  oenassex  43280  safesnsupfilb  43380  ifpim1  43431  ifpnot  43432  ifpid2  43433  ifpim2  43434  ifpxorcor  43438  ifpnot23  43440  ifpananb  43468  ifpnannanb  43469  ifpxorxorb  43473  rp-fakeinunass  43477  snen1g  43486  pren2  43515  alephiso2  43520  undmrnresiss  43566  cnvssco  43568  cotrintab  43576  cnviun  43612  imaiun1  43613  coiun1  43614  elintima  43615  frege133d  43727  frege54cor0a  43825  or3or  43985  andi3or  43986  ntrneik4w  44062  k0004lem1  44109  ismnuprim  44256  ismnushort  44263  undisjrab  44268  nzss  44279  pm10.541  44329  compab  44404  onfrALTlem5  44505  onfrALTlem5VD  44847  rext0  44901  wfaxun  44962  brpermmodel  44966  permaxrep  44969  permaxpow  44972  permac8prim  44977  eluni2f  45070  euabsneu  47002  aiotaexb  47063  aiotavb  47064  r19.32  47072  3an4ancom24  47243  ichn  47430  ichcom  47433  ichbi12i  47434  prproropf1olem0  47476  pairreueq  47484  clnbgrsym  47811  usgrexmpl2nb0  47995  usgrexmpl2nb1  47996  usgrexmpl2nb2  47997  usgrexmpl2nb3  47998  usgrexmpl2nb4  47999  usgrexmpl2nb5  48000  sgrp2sgrp  48189  islindeps  48415  elbigo  48513  reutruALT  48766  coxp  48794  tposres0  48838  catcinv  49361  isthincd2  49399  setrec1lem3  49651  elpg  49676