Theorem 3bitr4i 306

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 281	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitri 278	1 ⊢ (𝜒 ↔ 𝜃)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  bibi2d  345  pm4.71  566  pm5.32ri  585  an31  660  pm4.14  818  or4  939  orimdi  943  orbidi  967  ordi  1021  ordir  1022  andir  1024  dfbi3  1063  dfifp7  1083  ifpdfbiOLD  1085  ifpn  1088  3orrot  1106  3orcoma  1107  3ioran  1121  3ianor  1122  3anbi123i  1171  3orbi123i  1172  3jaob  1451  an6  1471  3or6  1473  an3andi  1510  an33rean  1511  nancom  1523  xorass  1542  anxordi  1553  norass  1564  hadbi  1625  hadcoma  1626  hadcomb  1627  hadnot  1629  cador  1635  cadan  1636  cadcoma  1639  cadnot  1642  nic-axALT  1701  19.26-3an  1899  19.43OLD  1910  19.32v  1967  19.31v  1968  19.42v  1980  4exdistr  1988  cbvexvw  2064  exexw  2080  sb3an  2121  sbcom4  2129  sbbiiev  2133  excom  2203  sbal  2210  19.32  2275  19.31  2276  19.42  2278  equsalv  2309  sbex  2322  sbrim  2345  sbor  2347  sbbi  2348  cbvex2v  2382  eeeanv  2388  sbnf2  2396  cbvsbvf  2401  cbvex2  2450  equsal  2455  dfsb3  2532  mo4  2600  eu6  2608  dfeu  2629  sb8eulem  2632  sb8mo  2635  cbvmovw  2636  cbvmow  2637  cbveuvw  2639  cbveuw  2640  cbveuALT  2642  eu1  2644  sbmo  2648  cbvabv  2839  cbvabw  2840  cbvab  2841  eqabcbw  2843  eqabcb  2909  nfceqi  2928  ralbii2  3113  rexbii2  3114  r19.26-3  3132  r19.43  3139  r2allem  3159  r19.42v  3203  r19.32v  3204  reeanlem  3242  3reeanv  3244  cbvralvw  3249  cbvrexvw  3250  ralcom  3299  ralcomf  3309  rexcomf  3310  cbvralfw  3311  cbvralsvw  3322  cbvralf  3356  cbvrexf  3357  reu5  3378  rmobiia  3382  reubiia  3383  rmo5  3394  cbvrmovw  3397  cbvreuvw  3398  cbvrmow  3401  cbvreuw  3402  cbvreu  3415  cbvrmo  3416  rabid2f  3454  abv  3475  abvALT  3476  ceqsal  3500  ceqsalv  3502  ceqsex3v  3515  ceqsex4v  3516  ceqsex8v  3518  reurab  3673  eueq  3680  reu2  3697  reu6  3698  reu3  3699  rmo4  3702  rmo3f  3706  2reu5  3730  cbvsbcw  3786  cbvsbcvw  3787  cbvsbc  3788  sbc3an  3817  sbccomlemOLD  3832  rmo3  3851  rmoanim  3856  rmoanimALT  3857  cbvralcsf  3903  cbvrexcsf  3904  cbvreucsf  3905  eqss  3960  uniiunlem  4049  sspsstri  4068  compleq  4114  ssequn1  4147  unss  4151  rexun  4157  ralunb  4158  elin3  4167  inass  4188  ssin  4199  elsymdif  4219  nssinpss  4228  dfun2  4231  difin  4233  indi  4245  indifdi  4255  difin2  4262  eq0  4312  ssdif0  4329  inn0f  4334  inssdif0  4337  ab0w  4342  ab0  4343  ab0orv  4346  abn0  4348  rabeq0w  4351  rabeq0  4352  disj3  4420  ssundif  4453  ralidmw  4482  dfif2  4494  eldifpr  4629  rexdifpr  4630  rexsns  4642  snprc  4688  reusn  4698  difsnpss  4779  tpss  4806  pwpr  4870  eluni2  4880  elunirab  4891  uniun  4899  unissb  4910  elintrab  4929  ssintrab  4940  intun  4949  iuncom  4968  iuncom4  4969  iunab  5020  ssiinf  5023  iunn0  5035  iinab  5036  iunin2  5039  iinun2  5041  iundif2  5042  iunun  5063  iunxun  5064  iunxiun  5067  sspwuni  5070  iinpw  5076  cbvdisj  5090  cbvdisjv  5091  disjor  5095  brun  5166  brin  5167  brdif  5168  dftr2  5224  dftr5  5226  intexrab  5318  inuni  5321  ssext  5436  pweqb  5438  otth2  5466  otthne  5469  propeqop  5491  vopelopabsb  5514  eqopab2bw  5534  eqopab2b  5538  pwin  5553  pwun  5555  dffr6  5618  elxp2  5686  otelxp  5706  xpiundi  5733  xpiundir  5734  poinxp  5743  soinxp  5744  frinxp  5745  seinxp  5746  weinxp  5747  reliun  5804  inopab  5817  difopab  5818  inxp  5819  raliunxp  5826  rexiunxp  5827  rexxpf  5834  iunxpf  5835  cnvco  5876  dmiun  5904  dmuni  5905  dm0rn0  5915  dm0rn0OLD  5916  dmres  6012  restidsing  6056  asymref  6117  codir  6121  qfto  6122  cnvopab  6138  cnvdif  6141  rniun  6146  dminss  6151  imainss  6152  difxp  6162  xpdifid  6166  xpdifcnvepel  6167  dmsnn0  6209  cnvcnvsn  6221  cnvresima  6232  resco  6252  imaco  6253  rnco  6254  rncoOLD  6255  coiun  6259  coass  6268  ressn  6287  cnviin  6288  cnvpo  6289  cnvso  6290  xpco  6291  opreu2reurex  6296  dfpo2  6298  imaindm  6301  dflim2  6420  funcnv  6606  funcnv3  6607  fncnv  6610  fun11  6611  imadif  6621  fnres  6663  dfmpt3  6670  mptfnf  6671  fnopabg  6673  fint  6758  fin  6759  fores  6803  dff1o3  6828  f1ompt  7107  fsn  7132  imaiun  7244  isocnv2  7330  isocnv3  7331  isores2  7332  isomin  7336  eqoprab2bw  7481  eqoprab2b  7482  elpwpwel  7765  sucexb  7802  onsucb  7812  dflim4  7843  fiun  7939  f1iun  7940  f11o  7943  opabex3d  7961  opabex3rd  7962  opabex3  7963  dfopab2  8048  dfoprab3s  8049  fmpox  8063  fparlem1  8106  fparlem2  8107  tpostpos  8241  frrlem9  8290  dfsmo2  8333  brwitnlem  8491  oarec  8546  naddasslem1  8680  naddasslem2  8681  qsid  8778  uniinqs  8794  mapval2  8869  mapsncnv  8890  elixp2  8898  ixpin  8920  brsdom  8970  brdom2  8978  xpassen  9058  brsdom2  9088  unfilem1  9264  fiint  9285  dfsup2  9403  supmo  9411  eqinf  9444  infmo  9456  brttrcl2  9682  rankc1  9841  cp  9876  isinfcard  10075  aceq1  10100  aceq2  10102  dfac5lem3  10108  dfac10b  10122  dfac12a  10131  dffin7-2  10381  dfacfin7  10382  fin1a2lem6  10388  iunfo  10522  konigthlem  10552  axgroth6  10812  axgroth3  10815  sstskm  10826  ltexprlem1  11020  gt0srpr  11062  ltpsrpr  11093  map2psrpr  11094  ltresr  11124  fimaxre3  12160  sup3  12171  supaddc  12181  supmul1  12183  elnn0z  12603  elznn0nn  12604  zmin  12967  xrnemnf  13141  xrnepnf  13142  dfrp2  13420  elioomnf  13470  elxrge0  13483  elfzuzb  13545  fzass4  13589  elfz2nn0  13645  elfzo2  13689  elfzo3  13704  lbfzo0  13727  fzo1lb  13741  fzind2  13816  nn0opthlem1  14303  hashgt23el  14460  cotr2g  15012  rexfiuz  15398  fsumcom2  15824  prodmo  15989  fprodcom2  16037  sinltx  16244  divalglem4  16453  divalglem10  16459  4sqlem12  17015  imasleval  17594  xpsfrnel  17615  xpscf  17618  isssc  17876  isffth2  17974  ispos2  18370  issubmgm  18759  ismhm  18842  issubmndb  18862  nsgacs  19227  isgim  19331  oppgcntz  19433  f1omvdco3  19518  pmtrprfvalrn  19557  efgrelexlemb  19819  pgpfac1  20151  pgpfac  20155  issrg  20269  opprsubg  20433  opprunit  20458  isirred2  20502  opprirred  20503  opprnzrb  20604  opprdomnb  20800  isdomn4r  20802  drngprop  20827  opprdrng  20845  issdrg2  20875  isorng  20941  islss  21032  islbs  21174  prmidl0  21446  unocv  21798  iunocv  21799  isbasis2g  23073  tgval2  23081  ntreq0  23202  isclo2  23213  cmpcov2  23515  is1stc2  23567  1stcelcls  23586  llyi  23599  unisngl  23652  txuni2  23690  xkobval  23711  hausdiag  23770  isfbas2  23960  elfg  23996  fbasrn  24009  fmfnfmlem3  24081  isfcls  24134  alexsubALTlem2  24173  istmd  24199  istgp  24202  istrg  24289  istdrg  24291  istdrg2  24303  isms2  24575  metuel2  24690  restmetu  24695  isngp  24721  isngp2  24722  isngp3  24723  elii1  25062  isncvsngp  25276  iscph  25297  isbn  25465  pmltpc  25577  ovolfcl  25593  finiunmbl  25671  iundisj  25675  dyaddisj  25723  vitalilem1  25735  ellimc3  26006  ig1pval3  26303  plyun0  26322  plydivex  26426  aannenlem2  26458  ellogrn  26689  atandm  27006  atandm3  27008  atans2  27061  elno3  27784  conway  27937  eqcuts2  27944  madeval2  27991  ons2ind  28433  tgjustf  28707  colinearalg  29200  axeuclid  29253  nbgrsym  29653  upgrtrls  29989  upgristrl  29990  dfpth2  30018  usgr2pth0  30054  iswwlks  30125  isclwwlk  30275  clwwlkneq0  30320  h2hlm  31272  issh  31500  chcon2i  31756  chcon1i  31757  chcon3i  31758  chnlei  31777  cmcm2i  31885  cmcm3i  31886  3oalem3  31956  pjdifnormii  31975  pjneli  32015  dfadj2  32177  cnvadj  32184  hhcno  32196  hhcnf  32197  eleigvec  32249  eleigvec2  32250  pjimai  32468  isst  32505  ishst  32506  cvnbtwn4  32581  chrelat4i  32665  2reucom  32766  reuxfrdf  32777  difrab2  32784  inpr0  32818  iunin1f  32842  disjnf  32855  cbvdisjf  32856  disjorf  32864  iundisjf  32874  disjexc  32878  xrdifh  33065  iundisjfi  33081  hashxpe  33092  pmtrprfv2  33348  xrnarchi  33444  isunit2  33499  opprnsg  33710  ccfldextdgrr  34006  cmpcref  34184  ordtconnlem1  34258  isrrext  34334  cntnevol  34562  ddemeas  34570  omssubaddlem  34633  omssubadd  34634  eulerpartleme  34697  eulerpartlemv  34698  eulerpartlemt0  34703  eulerpartlemgvv  34710  eulerpartlemn  34715  ballotlem2  34823  ballotlemodife  34832  oddprm2  34986  bnj257  35040  bnj268  35042  bnj290  35043  bnj312  35045  bnj89  35054  bnj887  35098  bnj976  35110  bnj1019  35112  bnj1146  35123  bnj1385  35164  bnj110  35190  bnj121  35202  bnj130  35206  bnj153  35212  bnj543  35225  bnj580  35245  bnj607  35248  bnj849  35257  bnj882  35258  bnj916  35265  bnj985v  35285  bnj985  35286  bnj1033  35301  bnj1083  35310  bnj1090  35311  bnj1128  35322  bnj1174  35335  bnj1228  35343  onvf1odlem1  35485  erdszelem1  35581  cvmliftlem15  35688  snmlval  35721  satfvsuclem2  35750  satfdm  35759  elmpst  35926  mpstrcl  35931  orbi2iALT  36075  untuni  36099  dfso3  36110  xpab  36116  dftr6  36141  coep  36142  coepr  36143  dffr5  36144  dfso2  36145  cnvco1  36149  cnvco2  36150  eldm3  36151  dfdm5  36163  dfrn5  36164  brsset  36277  idsset  36278  dfon3  36280  dfbigcup2  36287  dfom5b  36300  dffun10  36302  dfiota3  36311  fnimage  36317  brdomain  36321  brrange  36322  brimg  36325  brapply  36326  brcup  36327  brcap  36328  lemsuccf  36329  funpartlem  36332  brrestrict  36339  dfrecs2  36340  brub  36344  altopelaltxp  36366  rmoeqi  36587  rmoeqbii  36588  reueqi  36589  reueqbii  36590  sbceqbii  36591  disjeq1i  36592  cbvralvw2  36626  cbvrexvw2  36627  cbvrmovw2  36628  cbvreuvw2  36629  cbvsbcvw2  36630  cbvdisjvw2  36635  trer  36715  filnetlem4  36780  df3nandALT1  36798  imnand2  36801  mh-unprimbi  36943  bj-dfbi5  37055  bj-bixor  37072  bj-dfsbc  37162  bj-nnfnt  37263  bj-csbsnlem  37426  bj-rcleqf  37548  bj-sscon  37552  bj-pw0ALT  37572  bj-restpw  37621  bj-opelidb1  37684  bj-imdiridlem  37716  bj-imdirco  37721  wl-df3xor2  38002  wl-3xorrot  38010  wl-3xorcoma  38011  wl-3xornot  38014  wl-df2-3mintru2  38018  wl-df3-3mintru2  38019  wl-df4-3mintru2  38020  wl-equsalvw  38080  wl-sb9v  38091  iundif1  38132  poimirlem25  38183  poimirlem26  38184  poimirlem30  38188  ismblfin  38199  mbfposadd  38205  itg2addnclem2  38210  ftc1anc  38239  inixp  38266  prdstotbnd  38332  heibor1lem  38347  isrngohom  38503  isidl  38552  isfldidl2  38607  isdmn3  38612  sbccom2lem  38662  triantru3  38774  vvdifopab  38803  brres2  38811  eldmqsres  38831  inxpss  38855  ref5  38857  n0el2  38873  dfsucmap3  39001  trcoss2  39112  dfeqvrel2  39212  dfeqvrel3  39213  redundeq1  39251  redundpbi1  39253  refrelredund4  39257  funALTVfun  39321  dfeldisj3  39349  dfeldisj5  39351  pet0  39456  petid  39458  petidres  39460  petinidres  39462  petxrnidres  39464  mpet  39491  petincnvepres  39501  pet  39503  pmapglbx  40432  lhpexle3  40675  cdleme25cv  41021  dicelval3  41843  diclspsn  41857  lcfls1c  42199  sn-axrep5v  42877  sn-iotalem  42881  psspwb  42888  redvmptabs  43010  eu6w  43299  moxfr  43314  fphpd  43434  uniel  43835  dflim6  43882  onsucf1olem  43888  dflim7  43891  omge2  43916  oenassex  43936  safesnsupfilb  44035  ifpim1  44086  ifpnot  44087  ifpid2  44088  ifpim2  44089  ifpxorcor  44093  ifpnot23  44095  ifpananb  44123  ifpnannanb  44124  ifpxorxorb  44128  rp-fakeinunass  44132  snen1g  44141  pren2  44170  alephiso2  44175  undmrnresiss  44221  cnvssco  44223  cotrintab  44231  cnviun  44267  imaiun1  44268  coiun1  44269  elintima  44270  frege133d  44382  frege54cor0a  44480  or3or  44640  andi3or  44641  ntrneik4w  44717  k0004lem1  44764  ismnuprim  44895  ismnushort  44902  undisjrab  44907  nzss  44918  pm10.541  44968  compab  45042  onfrALTlem5  45142  onfrALTlem5VD  45484  rext0  45538  wfaxun  45599  brpermmodel  45603  permaxrep  45606  permaxpow  45609  permac8prim  45614  eluni2f  45712  euabsneu  47653  aiotaexb  47714  aiotavb  47715  r19.32  47723  3an4ancom24  47894  ichn  48093  ichcom  48096  ichbi12i  48097  prproropf1olem0  48139  pairreueq  48147  clnbgrsym  48491  usgrexmpl2nb0  48684  usgrexmpl2nb1  48685  usgrexmpl2nb2  48686  usgrexmpl2nb3  48687  usgrexmpl2nb4  48688  usgrexmpl2nb5  48689  sgrp2sgrp  48881  islindeps  49117  elbigo  49215  reutruALT  49467  coxp  49495  tposres0  49539  catcinv  50061  isthincd2  50099  setrec1lem3  50351  elpg  50376  dfrals2  50452  alsbii  50462  ralsbii  50463  cbvals  50467