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  807  or4  927  orimdi  931  orbidi  955  ordi  1008  ordir  1009  andir  1011  dfbi3  1050  dfifp7  1070  ifpdfbi  1071  ifpn  1074  3orrot  1092  3orcoma  1093  3ioran  1106  3ianor  1107  3anbi123i  1156  3orbi123i  1157  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  2036  exexw  2051  sb3an  2081  sbcom4  2089  sbbiiev  2092  excom  2162  sbal  2169  19.32  2233  19.31  2234  19.42  2236  equsalv  2267  sbex  2281  sbrim  2304  sbor  2307  sbbi  2308  sbnfOLD  2313  cbvex2v  2346  eeeanv  2352  sbnf2  2361  cbvsbvf  2366  cbvex2  2417  equsal  2422  dfsb3  2499  mo4  2566  eu6  2574  eubii  2585  dfeu  2595  sb8eulem  2598  sb8mo  2601  cbvmovw  2602  cbvmow  2603  cbveuvw  2605  cbveuw  2606  cbveuALT  2608  eu1  2610  sbmo  2614  cbvabv  2812  cbvabw  2813  cbvab  2814  eqabcb  2883  nfceqi  2902  sbabelOLD  2939  ralbii2  3089  rexbii2  3090  r19.26-3  3112  r19.43  3122  r2allem  3142  r19.21vOLD  3181  r19.42v  3191  r19.32v  3192  reeanlem  3228  3reeanv  3230  2ralorOLD  3232  cbvralvw  3237  cbvrexvw  3238  ralcom4OLD  3287  ralcom  3289  ralcomf  3302  rexcomf  3303  cbvralfw  3304  cbvralsvw  3317  cbvralf  3360  cbvrexf  3361  reu5  3382  rmobiia  3386  reubiia  3387  rmoanidOLD  3392  reuanidOLD  3393  rmo5  3400  cbvrmovw  3403  cbvreuvw  3404  moelOLD  3405  cbvrmow  3409  cbvreuw  3410  cbvreuwOLD  3415  cbvreu  3428  cbvrmo  3429  rabid2f  3468  rabid2OLD  3471  abv  3492  abvALT  3493  ceqsal  3519  ceqsalv  3521  cgsex4gOLD  3529  ceqsex3v  3537  ceqsex4v  3538  ceqsex8v  3540  reurab  3707  eueq  3714  reu2  3731  reu6  3732  reu3  3733  rmo4  3736  rmo3f  3740  2reu5  3764  cbvsbcw  3821  cbvsbcvw  3822  cbvsbc  3823  sbc3an  3855  sbccomlemOLD  3870  rmo3  3889  rmoanim  3894  rmoanimALT  3895  cbvralcsf  3941  cbvrexcsf  3942  cbvreucsf  3943  eqss  3999  uniiunlem  4087  sspsstri  4105  compleq  4152  ssequn1  4186  unss  4190  rexun  4196  ralunb  4197  elin3  4206  inass  4228  ssin  4239  elsymdif  4258  nssinpss  4267  dfun2  4270  difin  4272  indi  4284  indifdi  4294  difin2  4301  ssdif0  4366  inn0f  4371  inssdif0  4374  ab0  4380  abn0  4385  rabeq0w  4387  rabeq0  4388  disj  4450  disj3  4454  ssundif  4488  ralidmw  4508  dfif2  4527  eldifpr  4658  rexdifpr  4659  rexsns  4671  snprc  4717  reusn  4727  difsnpss  4807  tpss  4837  pwpr  4901  eluni2  4911  elunirab  4922  uniun  4930  unissb  4939  unissbOLD  4940  elintrab  4960  ssintrab  4971  intun  4980  iuncom  4999  iuncom4  5000  iunab  5051  ssiinf  5054  iunn0  5067  iinab  5068  iunin2  5071  iinun2  5073  iundif2  5074  iunun  5093  iunxun  5094  iunxiun  5097  sspwuni  5100  iinpw  5106  cbvdisj  5120  cbvdisjv  5121  disjor  5125  brun  5194  brin  5195  brdif  5196  dftr2  5261  dftr5  5263  intexrab  5347  inuni  5350  ssext  5459  pweqb  5461  otth2  5488  otthne  5491  propeqop  5512  vopelopabsb  5534  eqopab2bw  5553  eqopab2b  5557  pwin  5574  pwun  5576  dffr6  5640  elxp2  5709  otelxp  5729  xpiundi  5756  xpiundir  5757  poinxp  5766  soinxp  5767  frinxp  5768  seinxp  5769  weinxp  5770  inopab  5839  difopab  5840  difopabOLD  5841  inxp  5842  raliunxp  5850  rexiunxp  5851  rexxpf  5858  iunxpf  5859  cnvco  5896  dmiun  5924  dmuni  5925  dm0rn0  5935  dmres  6030  restidsing  6071  cnvsymOLDOLD  6134  asymref  6136  codir  6140  qfto  6141  cnvopab  6157  cnvopabOLD  6158  cnvdif  6163  rniun  6167  dminss  6173  imainss  6174  difxp  6184  xpdifid  6188  dmsnn0  6227  cnvcnvsn  6239  cnvresima  6250  resco  6270  imaco  6271  rnco  6272  coiun  6276  coass  6285  ressn  6305  cnviin  6306  cnvpo  6307  cnvso  6308  xpco  6309  opreu2reurex  6314  dfpo2  6316  imaindm  6319  dflim2  6441  funcnv  6635  funcnv3  6636  fncnv  6639  fun11  6640  imadif  6650  fnres  6695  dfmpt3  6702  mptfnf  6703  fnopabg  6705  fint  6787  fin  6788  fores  6830  dff1o3  6854  f1ompt  7131  fsn  7155  imaiun  7265  isocnv2  7351  isocnv3  7352  isores2  7353  isomin  7357  eqoprab2bw  7503  eqoprab2b  7504  elpwpwel  7787  sucexb  7824  onsucb  7837  dflim4  7869  fiun  7967  f1iun  7968  f11o  7971  opabex3d  7990  opabex3rd  7991  opabex3  7992  dfopab2  8077  dfoprab3s  8078  fmpox  8092  fparlem1  8137  fparlem2  8138  tpostpos  8271  frrlem9  8319  wfrlem8OLD  8356  wfrfunOLD  8359  dfsmo2  8387  brwitnlem  8545  oarec  8600  naddasslem1  8732  naddasslem2  8733  qsid  8823  uniinqs  8837  mapval2  8912  mapsncnv  8933  elixp2  8941  ixpin  8963  brsdom  9015  brdom2  9022  xpassen  9106  brsdom2  9137  dif1enOLD  9202  unfilem1  9343  fiint  9366  fiintOLD  9367  dfsup2  9484  supmo  9492  eqinf  9524  infmo  9535  brttrcl2  9754  rankc1  9910  cp  9931  isinfcard  10132  aceq1  10157  aceq2  10159  dfac5lem3  10165  dfac10b  10180  dfac12a  10189  dffin7-2  10438  dfacfin7  10439  fin1a2lem6  10445  iunfo  10579  konigthlem  10608  axgroth6  10868  axgroth3  10871  sstskm  10882  ltexprlem1  11076  gt0srpr  11118  ltpsrpr  11149  map2psrpr  11150  ltresr  11180  fimaxre3  12214  sup3  12225  supaddc  12235  supmul1  12237  elnn0z  12626  elznn0nn  12627  zmin  12986  xrnemnf  13159  xrnepnf  13160  dfrp2  13436  elioomnf  13484  elxrge0  13497  elfzuzb  13558  fzass4  13602  elfz2nn0  13658  elfzo2  13702  elfzo3  13716  lbfzo0  13739  fzo1lb  13753  fzind2  13824  nn0opthlem1  14307  hashgt23el  14463  cotr2g  15015  rexfiuz  15386  fsumcom2  15810  prodmo  15972  fprodcom2  16020  sinltx  16225  divalglem4  16433  divalglem10  16439  4sqlem12  16994  imasleval  17586  xpsfrnel  17607  xpscf  17610  isssc  17864  isffth2  17963  ispos2  18361  issubmgm  18715  ismhm  18798  issubmndb  18818  nsgacs  19180  isgim  19280  oppgcntz  19383  f1omvdco3  19467  pmtrprfvalrn  19506  efgrelexlemb  19768  pgpfac1  20100  pgpfac  20104  issrg  20185  opprsubg  20352  opprunit  20377  isirred2  20421  opprirred  20422  opprnzrb  20521  isdomn2OLD  20712  opprdomnb  20717  isdomn4r  20719  drngprop  20744  opprdrng  20764  issdrg2  20796  islss  20932  islbs  21075  unocv  21698  iunocv  21699  isbasis2g  22955  tgval2  22963  ntreq0  23085  isclo2  23096  cmpcov2  23398  is1stc2  23450  1stcelcls  23469  llyi  23482  unisngl  23535  txuni2  23573  xkobval  23594  hausdiag  23653  isfbas2  23843  elfg  23879  fbasrn  23892  fmfnfmlem3  23964  isfcls  24017  alexsubALTlem2  24056  istmd  24082  istgp  24085  istrg  24172  istdrg  24174  istdrg2  24186  isms2  24460  metuel2  24578  restmetu  24583  isngp  24609  isngp2  24610  isngp3  24611  elii1  24964  isncvsngp  25183  iscph  25204  isbn  25372  pmltpc  25485  ovolfcl  25501  finiunmbl  25579  iundisj  25583  dyaddisj  25631  vitalilem1  25643  ellimc3  25914  ig1pval3  26217  plyun0  26236  plydivex  26339  aannenlem2  26371  ellogrn  26601  atandm  26919  atandm3  26921  atans2  26974  elno3  27700  conway  27844  eqscut2  27851  madeval2  27892  tgjustf  28481  colinearalg  28925  axeuclid  28978  nbgrsym  29380  upgrtrls  29719  upgristrl  29720  dfpth2  29749  usgr2pth0  29785  iswwlks  29856  isclwwlk  30003  clwwlkneq0  30048  h2hlm  30999  issh  31227  chcon2i  31483  chcon1i  31484  chcon3i  31485  chnlei  31504  cmcm2i  31612  cmcm3i  31613  3oalem3  31683  pjdifnormii  31702  pjneli  31742  dfadj2  31904  cnvadj  31911  hhcno  31923  hhcnf  31924  eleigvec  31976  eleigvec2  31977  pjimai  32195  isst  32232  ishst  32233  cvnbtwn4  32308  chrelat4i  32392  2reucom  32499  reuxfrdf  32510  difrab2  32517  inpr0  32550  iunin1f  32570  disjnf  32583  cbvdisjf  32584  disjorf  32592  iundisjf  32602  disjexc  32606  xrdifh  32782  iundisjfi  32798  hashxpe  32811  pmtrprfv2  33108  xrnarchi  33191  isunit2  33244  isorng  33329  prmidl0  33478  opprnsg  33512  ccfldextdgrr  33722  cmpcref  33849  ordtconnlem1  33923  isrrext  34001  cntnevol  34229  ddemeas  34237  omssubaddlem  34301  omssubadd  34302  eulerpartleme  34365  eulerpartlemv  34366  eulerpartlemt0  34371  eulerpartlemgvv  34378  eulerpartlemn  34383  ballotlem2  34491  ballotlemodife  34500  oddprm2  34670  bnj257  34721  bnj268  34723  bnj290  34724  bnj312  34726  bnj89  34735  bnj887  34779  bnj976  34791  bnj1019  34793  bnj1146  34805  bnj1385  34846  bnj110  34872  bnj121  34884  bnj130  34888  bnj153  34894  bnj543  34907  bnj580  34927  bnj607  34930  bnj849  34939  bnj882  34940  bnj916  34947  bnj985v  34967  bnj985  34968  bnj1033  34983  bnj1083  34992  bnj1090  34993  bnj1128  35004  bnj1174  35017  bnj1228  35025  erdszelem1  35196  cvmliftlem15  35303  snmlval  35336  satfvsuclem2  35365  satfdm  35374  elmpst  35541  mpstrcl  35546  orbi2iALT  35690  untuni  35709  dfso3  35720  xpab  35726  dftr6  35751  coep  35752  coepr  35753  dffr5  35754  dfso2  35755  cnvco1  35759  cnvco2  35760  eldm3  35761  dfdm5  35773  dfrn5  35774  brsset  35890  idsset  35891  dfon3  35893  dfbigcup2  35900  dfom5b  35913  dffun10  35915  dfiota3  35924  fnimage  35930  brdomain  35934  brrange  35935  brimg  35938  brapply  35939  brcup  35940  brcap  35941  brsuccf  35942  funpartlem  35943  brrestrict  35950  dfrecs2  35951  brub  35955  altopelaltxp  35977  rmoeqi  36188  rmoeqbii  36189  reueqi  36190  reueqbii  36191  sbceqbii  36192  disjeq1i  36193  cbvralvw2  36227  cbvrexvw2  36228  cbvrmovw2  36229  cbvreuvw2  36230  cbvsbcvw2  36231  cbvdisjvw2  36236  trer  36317  filnetlem4  36382  df3nandALT1  36400  imnand2  36403  bj-dfbi5  36575  bj-bixor  36592  bj-nnfnt  36741  bj-csbsnlem  36904  bj-rcleqf  37026  bj-sscon  37030  bj-pw0ALT  37050  bj-restpw  37093  bj-opelidb1  37154  bj-imdiridlem  37186  bj-imdirco  37191  wl-df3xor2  37470  wl-3xorrot  37478  wl-3xorcoma  37479  wl-3xornot  37482  wl-df2-3mintru2  37486  wl-df3-3mintru2  37487  wl-df4-3mintru2  37488  wl-equsalvw  37539  wl-sb9v  37550  iundif1  37601  poimirlem25  37652  poimirlem26  37653  poimirlem30  37657  ismblfin  37668  mbfposadd  37674  itg2addnclem2  37679  ftc1anc  37708  inixp  37735  prdstotbnd  37801  heibor1lem  37816  isrngohom  37972  isidl  38021  isfldidl2  38076  isdmn3  38081  sbccom2lem  38131  triantru3  38231  vvdifopab  38261  brres2  38269  eldmqsres  38288  inxpss  38312  ref5  38314  n0el2  38334  trcoss2  38485  dfeqvrel2  38591  dfeqvrel3  38592  redundeq1  38630  redundpbi1  38632  refrelredund4  38636  funALTVfun  38699  dfeldisj3  38720  dfeldisj5  38722  pet0  38816  petid  38818  petidres  38820  petinidres  38822  petxrnidres  38824  mpet  38840  petincnvepres  38850  pet  38852  pmapglbx  39771  lhpexle3  40014  cdleme25cv  40360  dicelval3  41182  diclspsn  41196  lcfls1c  41538  sn-axrep5v  42255  sn-iotalem  42260  psspwb  42267  redvmptabs  42390  eu6w  42686  moxfr  42703  fphpd  42827  uniel  43229  dflim6  43277  onsucf1olem  43283  dflim7  43286  omge2  43311  oenassex  43331  safesnsupfilb  43431  ifpim1  43482  ifpnot  43483  ifpid2  43484  ifpim2  43485  ifpxorcor  43489  ifpnot23  43491  ifpananb  43519  ifpnannanb  43520  ifpxorxorb  43524  rp-fakeinunass  43528  snen1g  43537  pren2  43566  alephiso2  43571  undmrnresiss  43617  cnvssco  43619  cotrintab  43627  cnviun  43663  imaiun1  43664  coiun1  43665  elintima  43666  frege133d  43778  frege54cor0a  43876  or3or  44036  andi3or  44037  ntrneik4w  44113  k0004lem1  44160  ismnuprim  44313  ismnushort  44320  undisjrab  44325  nzss  44336  pm10.541  44386  compab  44461  onfrALTlem5  44562  onfrALTlem5VD  44905  rext0  44959  wfaxun  45016  eluni2f  45108  euabsneu  47040  aiotaexb  47101  aiotavb  47102  r19.32  47110  3an4ancom24  47281  ichn  47443  ichcom  47446  ichbi12i  47447  prproropf1olem0  47489  pairreueq  47497  clnbgrsym  47824  usgrexmpl2nb0  47990  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  sgrp2sgrp  48144  islindeps  48370  elbigo  48472  reutruALT  48725  coxp  48744  tposres0  48777  isthincd2  49086  setrec1lem3  49208  elpg  49233