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  3090  r19.43  3097  r2allem  3117  r19.42v  3161  r19.32v  3162  reeanlem  3200  3reeanv  3202  cbvralvw  3207  cbvrexvw  3208  ralcom  3257  ralcomf  3268  rexcomf  3269  cbvralfw  3270  cbvralsvw  3281  cbvralf  3325  cbvrexf  3326  reu5  3347  rmobiia  3351  reubiia  3352  rmoanidOLD  3357  reuanidOLD  3358  rmo5  3365  cbvrmovw  3368  cbvreuvw  3369  cbvrmow  3372  cbvreuw  3373  cbvreu  3388  cbvrmo  3389  rabid2f  3428  abv  3450  abvALT  3451  ceqsal  3476  ceqsalv  3478  cgsex4gOLD  3486  ceqsex3v  3494  ceqsex4v  3495  ceqsex8v  3497  reurab  3663  eueq  3670  reu2  3687  reu6  3688  reu3  3689  rmo4  3692  rmo3f  3696  2reu5  3720  cbvsbcw  3777  cbvsbcvw  3778  cbvsbc  3779  sbc3an  3809  sbccomlemOLD  3824  rmo3  3843  rmoanim  3848  rmoanimALT  3849  cbvralcsf  3895  cbvrexcsf  3896  cbvreucsf  3897  eqss  3953  uniiunlem  4040  sspsstri  4058  compleq  4105  ssequn1  4139  unss  4143  rexun  4149  ralunb  4150  elin3  4159  inass  4181  ssin  4192  elsymdif  4211  nssinpss  4220  dfun2  4223  difin  4225  indi  4237  indifdi  4247  difin2  4254  ssdif0  4319  inn0f  4324  inssdif0  4327  ab0  4333  abn0  4338  rabeq0w  4340  rabeq0  4341  disj  4403  disj3  4407  ssundif  4441  ralidmw  4461  dfif2  4480  eldifpr  4612  rexdifpr  4613  rexsns  4625  snprc  4671  reusn  4681  difsnpss  4761  tpss  4791  pwpr  4855  eluni2  4865  elunirab  4876  uniun  4884  unissb  4893  elintrab  4913  ssintrab  4924  intun  4933  iuncom  4952  iuncom4  4953  iunab  5003  ssiinf  5006  iunn0  5019  iinab  5020  iunin2  5023  iinun2  5025  iundif2  5026  iunun  5045  iunxun  5046  iunxiun  5049  sspwuni  5052  iinpw  5058  cbvdisj  5072  cbvdisjv  5073  disjor  5077  brun  5146  brin  5147  brdif  5148  dftr2  5204  dftr5  5206  intexrab  5289  inuni  5292  ssext  5401  pweqb  5403  otth2  5430  otthne  5433  propeqop  5454  vopelopabsb  5476  eqopab2bw  5495  eqopab2b  5499  pwin  5514  pwun  5516  dffr6  5579  elxp2  5647  otelxp  5667  xpiundi  5694  xpiundir  5695  poinxp  5704  soinxp  5705  frinxp  5706  seinxp  5707  weinxp  5708  inopab  5776  difopab  5777  inxp  5778  raliunxp  5786  rexiunxp  5787  rexxpf  5794  iunxpf  5795  cnvco  5832  dmiun  5860  dmuni  5861  dm0rn0  5871  dmres  5967  restidsing  6008  asymref  6069  codir  6073  qfto  6074  cnvopab  6090  cnvopabOLD  6091  cnvdif  6096  rniun  6100  dminss  6106  imainss  6107  difxp  6117  xpdifid  6121  dmsnn0  6160  cnvcnvsn  6172  cnvresima  6183  resco  6203  imaco  6204  rnco  6205  coiun  6209  coass  6218  ressn  6237  cnviin  6238  cnvpo  6239  cnvso  6240  xpco  6241  opreu2reurex  6246  dfpo2  6248  imaindm  6251  dflim2  6369  funcnv  6555  funcnv3  6556  fncnv  6559  fun11  6560  imadif  6570  fnres  6613  dfmpt3  6620  mptfnf  6621  fnopabg  6623  fint  6707  fin  6708  fores  6750  dff1o3  6774  f1ompt  7049  fsn  7073  imaiun  7185  isocnv2  7272  isocnv3  7273  isores2  7274  isomin  7278  eqoprab2bw  7423  eqoprab2b  7424  elpwpwel  7707  sucexb  7744  onsucb  7756  dflim4  7788  fiun  7885  f1iun  7886  f11o  7889  opabex3d  7907  opabex3rd  7908  opabex3  7909  dfopab2  7994  dfoprab3s  7995  fmpox  8009  fparlem1  8052  fparlem2  8053  tpostpos  8186  frrlem9  8234  dfsmo2  8277  brwitnlem  8432  oarec  8487  naddasslem1  8619  naddasslem2  8620  qsid  8715  uniinqs  8731  mapval2  8806  mapsncnv  8827  elixp2  8835  ixpin  8857  brsdom  8907  brdom2  8914  xpassen  8995  brsdom2  9025  dif1enOLD  9086  unfilem1  9212  fiint  9235  fiintOLD  9236  dfsup2  9353  supmo  9361  eqinf  9394  infmo  9406  brttrcl2  9629  rankc1  9785  cp  9806  isinfcard  10005  aceq1  10030  aceq2  10032  dfac5lem3  10038  dfac10b  10053  dfac12a  10062  dffin7-2  10311  dfacfin7  10312  fin1a2lem6  10318  iunfo  10452  konigthlem  10481  axgroth6  10741  axgroth3  10744  sstskm  10755  ltexprlem1  10949  gt0srpr  10991  ltpsrpr  11022  map2psrpr  11023  ltresr  11053  fimaxre3  12089  sup3  12100  supaddc  12110  supmul1  12112  elnn0z  12502  elznn0nn  12503  zmin  12863  xrnemnf  13037  xrnepnf  13038  dfrp2  13315  elioomnf  13365  elxrge0  13378  elfzuzb  13439  fzass4  13483  elfz2nn0  13539  elfzo2  13583  elfzo3  13597  lbfzo0  13620  fzo1lb  13634  fzind2  13706  nn0opthlem1  14193  hashgt23el  14349  cotr2g  14901  rexfiuz  15273  fsumcom2  15699  prodmo  15861  fprodcom2  15909  sinltx  16116  divalglem4  16325  divalglem10  16331  4sqlem12  16886  imasleval  17463  xpsfrnel  17484  xpscf  17487  isssc  17745  isffth2  17843  ispos2  18239  issubmgm  18594  ismhm  18677  issubmndb  18697  nsgacs  19059  isgim  19159  oppgcntz  19261  f1omvdco3  19346  pmtrprfvalrn  19385  efgrelexlemb  19647  pgpfac1  19979  pgpfac  19983  issrg  20091  opprsubg  20255  opprunit  20280  isirred2  20324  opprirred  20325  opprnzrb  20424  isdomn2OLD  20615  opprdomnb  20620  isdomn4r  20622  drngprop  20647  opprdrng  20667  issdrg2  20698  isorng  20764  islss  20855  islbs  20998  unocv  21605  iunocv  21606  isbasis2g  22851  tgval2  22859  ntreq0  22980  isclo2  22991  cmpcov2  23293  is1stc2  23345  1stcelcls  23364  llyi  23377  unisngl  23430  txuni2  23468  xkobval  23489  hausdiag  23548  isfbas2  23738  elfg  23774  fbasrn  23787  fmfnfmlem3  23859  isfcls  23912  alexsubALTlem2  23951  istmd  23977  istgp  23980  istrg  24067  istdrg  24069  istdrg2  24081  isms2  24354  metuel2  24469  restmetu  24474  isngp  24500  isngp2  24501  isngp3  24502  elii1  24847  isncvsngp  25065  iscph  25086  isbn  25254  pmltpc  25367  ovolfcl  25383  finiunmbl  25461  iundisj  25465  dyaddisj  25513  vitalilem1  25525  ellimc3  25796  ig1pval3  26099  plyun0  26118  plydivex  26221  aannenlem2  26253  ellogrn  26484  atandm  26802  atandm3  26804  atans2  26857  elno3  27583  conway  27728  eqscut2  27735  madeval2  27781  tgjustf  28436  colinearalg  28873  axeuclid  28926  nbgrsym  29326  upgrtrls  29663  upgristrl  29664  dfpth2  29692  usgr2pth0  29728  iswwlks  29799  isclwwlk  29946  clwwlkneq0  29991  h2hlm  30942  issh  31170  chcon2i  31426  chcon1i  31427  chcon3i  31428  chnlei  31447  cmcm2i  31555  cmcm3i  31556  3oalem3  31626  pjdifnormii  31645  pjneli  31685  dfadj2  31847  cnvadj  31854  hhcno  31866  hhcnf  31867  eleigvec  31919  eleigvec2  31920  pjimai  32138  isst  32175  ishst  32176  cvnbtwn4  32251  chrelat4i  32335  2reucom  32442  reuxfrdf  32453  difrab2  32460  inpr0  32494  iunin1f  32519  disjnf  32532  cbvdisjf  32533  disjorf  32541  iundisjf  32551  disjexc  32555  xrdifh  32736  iundisjfi  32752  hashxpe  32765  pmtrprfv2  33043  xrnarchi  33139  isunit2  33193  prmidl0  33400  opprnsg  33434  ccfldextdgrr  33646  cmpcref  33819  ordtconnlem1  33893  isrrext  33969  cntnevol  34197  ddemeas  34205  omssubaddlem  34269  omssubadd  34270  eulerpartleme  34333  eulerpartlemv  34334  eulerpartlemt0  34339  eulerpartlemgvv  34346  eulerpartlemn  34351  ballotlem2  34459  ballotlemodife  34468  oddprm2  34625  bnj257  34676  bnj268  34678  bnj290  34679  bnj312  34681  bnj89  34690  bnj887  34734  bnj976  34746  bnj1019  34748  bnj1146  34760  bnj1385  34801  bnj110  34827  bnj121  34839  bnj130  34843  bnj153  34849  bnj543  34862  bnj580  34882  bnj607  34885  bnj849  34894  bnj882  34895  bnj916  34902  bnj985v  34922  bnj985  34923  bnj1033  34938  bnj1083  34947  bnj1090  34948  bnj1128  34959  bnj1174  34972  bnj1228  34980  onvf1odlem1  35078  erdszelem1  35166  cvmliftlem15  35273  snmlval  35306  satfvsuclem2  35335  satfdm  35344  elmpst  35511  mpstrcl  35516  orbi2iALT  35660  untuni  35684  dfso3  35695  xpab  35701  dftr6  35726  coep  35727  coepr  35728  dffr5  35729  dfso2  35730  cnvco1  35734  cnvco2  35735  eldm3  35736  dfdm5  35748  dfrn5  35749  brsset  35865  idsset  35866  dfon3  35868  dfbigcup2  35875  dfom5b  35888  dffun10  35890  dfiota3  35899  fnimage  35905  brdomain  35909  brrange  35910  brimg  35913  brapply  35914  brcup  35915  brcap  35916  brsuccf  35917  funpartlem  35918  brrestrict  35925  dfrecs2  35926  brub  35930  altopelaltxp  35952  rmoeqi  36163  rmoeqbii  36164  reueqi  36165  reueqbii  36166  sbceqbii  36167  disjeq1i  36168  cbvralvw2  36202  cbvrexvw2  36203  cbvrmovw2  36204  cbvreuvw2  36205  cbvsbcvw2  36206  cbvdisjvw2  36211  trer  36292  filnetlem4  36357  df3nandALT1  36375  imnand2  36378  bj-dfbi5  36550  bj-bixor  36567  bj-nnfnt  36716  bj-csbsnlem  36879  bj-rcleqf  37001  bj-sscon  37005  bj-pw0ALT  37025  bj-restpw  37068  bj-opelidb1  37129  bj-imdiridlem  37161  bj-imdirco  37166  wl-df3xor2  37445  wl-3xorrot  37453  wl-3xorcoma  37454  wl-3xornot  37457  wl-df2-3mintru2  37461  wl-df3-3mintru2  37462  wl-df4-3mintru2  37463  wl-equsalvw  37514  wl-sb9v  37525  iundif1  37576  poimirlem25  37627  poimirlem26  37628  poimirlem30  37632  ismblfin  37643  mbfposadd  37649  itg2addnclem2  37654  ftc1anc  37683  inixp  37710  prdstotbnd  37776  heibor1lem  37791  isrngohom  37947  isidl  37996  isfldidl2  38051  isdmn3  38056  sbccom2lem  38106  triantru3  38206  vvdifopab  38237  brres2  38245  eldmqsres  38263  inxpss  38287  ref5  38289  n0el2  38305  trcoss2  38463  dfeqvrel2  38569  dfeqvrel3  38570  redundeq1  38608  redundpbi1  38610  refrelredund4  38614  funALTVfun  38678  dfeldisj3  38699  dfeldisj5  38701  pet0  38795  petid  38797  petidres  38799  petinidres  38801  petxrnidres  38803  mpet  38819  petincnvepres  38829  pet  38831  pmapglbx  39751  lhpexle3  39994  cdleme25cv  40340  dicelval3  41162  diclspsn  41176  lcfls1c  41518  sn-axrep5v  42192  sn-iotalem  42197  psspwb  42204  redvmptabs  42336  eu6w  42652  moxfr  42668  fphpd  42792  uniel  43193  dflim6  43240  onsucf1olem  43246  dflim7  43249  omge2  43274  oenassex  43294  safesnsupfilb  43394  ifpim1  43445  ifpnot  43446  ifpid2  43447  ifpim2  43448  ifpxorcor  43452  ifpnot23  43454  ifpananb  43482  ifpnannanb  43483  ifpxorxorb  43487  rp-fakeinunass  43491  snen1g  43500  pren2  43529  alephiso2  43534  undmrnresiss  43580  cnvssco  43582  cotrintab  43590  cnviun  43626  imaiun1  43627  coiun1  43628  elintima  43629  frege133d  43741  frege54cor0a  43839  or3or  43999  andi3or  44000  ntrneik4w  44076  k0004lem1  44123  ismnuprim  44270  ismnushort  44277  undisjrab  44282  nzss  44293  pm10.541  44343  compab  44418  onfrALTlem5  44519  onfrALTlem5VD  44861  rext0  44915  wfaxun  44976  brpermmodel  44980  permaxrep  44983  permaxpow  44986  permac8prim  44991  eluni2f  45084  euabsneu  47016  aiotaexb  47077  aiotavb  47078  r19.32  47086  3an4ancom24  47257  ichn  47444  ichcom  47447  ichbi12i  47448  prproropf1olem0  47490  pairreueq  47498  clnbgrsym  47826  usgrexmpl2nb0  48019  usgrexmpl2nb1  48020  usgrexmpl2nb2  48021  usgrexmpl2nb3  48022  usgrexmpl2nb4  48023  usgrexmpl2nb5  48024  sgrp2sgrp  48216  islindeps  48442  elbigo  48540  reutruALT  48793  coxp  48821  tposres0  48865  catcinv  49388  isthincd2  49426  setrec1lem3  49678  elpg  49703