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  1497  xorass  1516  anxordi  1527  norass  1538  hadbi  1599  hadcoma  1600  hadcomb  1601  hadnot  1603  cador  1609  cadan  1610  cadcoma  1613  cadnot  1616  nic-axALT  1675  19.26-3an  1873  19.43OLD  1884  19.32v  1941  19.31v  1942  19.42v  1954  4exdistr  1962  cbvexvw  2038  exexw  2054  sb3an  2086  sbcom4  2094  sbbiiev  2097  excom  2167  sbal  2174  19.32  2240  19.31  2241  19.42  2243  equsalv  2274  sbex  2287  sbrim  2310  sbor  2312  sbbi  2313  sbnfOLD  2318  cbvex2v  2348  eeeanv  2354  sbnf2  2362  cbvsbvf  2367  cbvex2  2416  equsal  2421  dfsb3  2498  mo4  2566  eu6  2574  dfeu  2595  sb8eulem  2598  sb8mo  2601  cbvmovw  2602  cbvmow  2603  cbveuvw  2605  cbveuw  2606  cbveuALT  2608  eu1  2610  sbmo  2614  cbvabv  2806  cbvabw  2807  cbvab  2808  eqabcbw  2810  eqabcb  2876  nfceqi  2895  ralbii2  3078  rexbii2  3079  r19.26-3  3097  r19.43  3104  r2allem  3124  r19.42v  3168  r19.32v  3169  reeanlem  3207  3reeanv  3209  cbvralvw  3214  cbvrexvw  3215  ralcom  3264  ralcomf  3274  rexcomf  3275  cbvralfw  3276  cbvralsvw  3287  cbvralf  3330  cbvrexf  3331  reu5  3352  rmobiia  3356  reubiia  3357  rmo5  3368  cbvrmovw  3371  cbvreuvw  3372  cbvrmow  3375  cbvreuw  3376  cbvreu  3391  cbvrmo  3392  rabid2f  3430  abv  3452  abvALT  3453  ceqsal  3478  ceqsalv  3480  cgsex4gOLD  3488  ceqsex3v  3495  ceqsex4v  3496  ceqsex8v  3498  reurab  3659  eueq  3666  reu2  3683  reu6  3684  reu3  3685  rmo4  3688  rmo3f  3692  2reu5  3716  cbvsbcw  3773  cbvsbcvw  3774  cbvsbc  3775  sbc3an  3805  sbccomlemOLD  3820  rmo3  3839  rmoanim  3844  rmoanimALT  3845  cbvralcsf  3891  cbvrexcsf  3892  cbvreucsf  3893  eqss  3949  uniiunlem  4039  sspsstri  4057  compleq  4104  ssequn1  4138  unss  4142  rexun  4148  ralunb  4149  elin3  4158  inass  4180  ssin  4191  elsymdif  4210  nssinpss  4219  dfun2  4222  difin  4224  indi  4236  indifdi  4246  difin2  4253  eq0  4302  ssdif0  4318  inn0f  4323  inssdif0  4326  ab0w  4331  ab0  4332  ab0orv  4335  abn0  4337  rabeq0w  4339  rabeq0  4340  disj3  4406  ssundif  4440  ralidmw  4469  dfif2  4481  eldifpr  4615  rexdifpr  4616  rexsns  4628  snprc  4674  reusn  4684  difsnpss  4763  tpss  4793  pwpr  4857  eluni2  4867  elunirab  4878  uniun  4886  unissb  4896  elintrab  4915  ssintrab  4926  intun  4935  iuncom  4954  iuncom4  4955  iunab  5007  ssiinf  5010  iunn0  5022  iinab  5023  iunin2  5026  iinun2  5028  iundif2  5029  iunun  5048  iunxun  5049  iunxiun  5052  sspwuni  5055  iinpw  5061  cbvdisj  5075  cbvdisjv  5076  disjor  5080  brun  5149  brin  5150  brdif  5151  dftr2  5207  dftr5  5209  intexrab  5292  inuni  5295  ssext  5402  pweqb  5404  otth2  5431  otthne  5434  propeqop  5455  vopelopabsb  5477  eqopab2bw  5496  eqopab2b  5500  pwin  5515  pwun  5517  dffr6  5580  elxp2  5648  otelxp  5668  xpiundi  5695  xpiundir  5696  poinxp  5705  soinxp  5706  frinxp  5707  seinxp  5708  weinxp  5709  reliun  5765  inopab  5778  difopab  5779  inxp  5780  raliunxp  5788  rexiunxp  5789  rexxpf  5796  iunxpf  5797  cnvco  5834  dmiun  5862  dmuni  5863  dm0rn0  5873  dm0rn0OLD  5874  dmres  5971  restidsing  6012  asymref  6073  codir  6077  qfto  6078  cnvopab  6094  cnvopabOLD  6095  cnvdif  6101  rniun  6105  dminss  6111  imainss  6112  difxp  6122  xpdifid  6126  dmsnn0  6165  cnvcnvsn  6177  cnvresima  6188  resco  6208  imaco  6209  rnco  6210  rncoOLD  6211  coiun  6215  coass  6224  ressn  6243  cnviin  6244  cnvpo  6245  cnvso  6246  xpco  6247  opreu2reurex  6252  dfpo2  6254  imaindm  6257  dflim2  6375  funcnv  6561  funcnv3  6562  fncnv  6565  fun11  6566  imadif  6576  fnres  6619  dfmpt3  6626  mptfnf  6627  fnopabg  6629  fint  6713  fin  6714  fores  6756  dff1o3  6780  f1ompt  7056  fsn  7080  imaiun  7191  isocnv2  7277  isocnv3  7278  isores2  7279  isomin  7283  eqoprab2bw  7428  eqoprab2b  7429  elpwpwel  7712  sucexb  7749  onsucb  7759  dflim4  7790  fiun  7887  f1iun  7888  f11o  7891  opabex3d  7909  opabex3rd  7910  opabex3  7911  dfopab2  7996  dfoprab3s  7997  fmpox  8011  fparlem1  8054  fparlem2  8055  tpostpos  8188  frrlem9  8236  dfsmo2  8279  brwitnlem  8434  oarec  8489  naddasslem1  8622  naddasslem2  8623  qsid  8718  uniinqs  8734  mapval2  8810  mapsncnv  8831  elixp2  8839  ixpin  8861  brsdom  8911  brdom2  8919  xpassen  8999  brsdom2  9029  unfilem1  9205  fiint  9227  dfsup2  9347  supmo  9355  eqinf  9388  infmo  9400  brttrcl2  9623  rankc1  9782  cp  9803  isinfcard  10002  aceq1  10027  aceq2  10029  dfac5lem3  10035  dfac10b  10050  dfac12a  10059  dffin7-2  10308  dfacfin7  10309  fin1a2lem6  10315  iunfo  10449  konigthlem  10479  axgroth6  10739  axgroth3  10742  sstskm  10753  ltexprlem1  10947  gt0srpr  10989  ltpsrpr  11020  map2psrpr  11021  ltresr  11051  fimaxre3  12088  sup3  12099  supaddc  12109  supmul1  12111  elnn0z  12501  elznn0nn  12502  zmin  12857  xrnemnf  13031  xrnepnf  13032  dfrp2  13310  elioomnf  13360  elxrge0  13373  elfzuzb  13434  fzass4  13478  elfz2nn0  13534  elfzo2  13578  elfzo3  13592  lbfzo0  13615  fzo1lb  13629  fzind2  13704  nn0opthlem1  14191  hashgt23el  14347  cotr2g  14899  rexfiuz  15271  fsumcom2  15697  prodmo  15859  fprodcom2  15907  sinltx  16114  divalglem4  16323  divalglem10  16329  4sqlem12  16884  imasleval  17462  xpsfrnel  17483  xpscf  17486  isssc  17744  isffth2  17842  ispos2  18238  issubmgm  18627  ismhm  18710  issubmndb  18730  nsgacs  19091  isgim  19191  oppgcntz  19293  f1omvdco3  19378  pmtrprfvalrn  19417  efgrelexlemb  19679  pgpfac1  20011  pgpfac  20015  issrg  20123  opprsubg  20288  opprunit  20313  isirred2  20357  opprirred  20358  opprnzrb  20454  isdomn2OLD  20645  opprdomnb  20650  isdomn4r  20652  drngprop  20677  opprdrng  20697  issdrg2  20728  isorng  20794  islss  20885  islbs  21028  unocv  21635  iunocv  21636  isbasis2g  22892  tgval2  22900  ntreq0  23021  isclo2  23032  cmpcov2  23334  is1stc2  23386  1stcelcls  23405  llyi  23418  unisngl  23471  txuni2  23509  xkobval  23530  hausdiag  23589  isfbas2  23779  elfg  23815  fbasrn  23828  fmfnfmlem3  23900  isfcls  23953  alexsubALTlem2  23992  istmd  24018  istgp  24021  istrg  24108  istdrg  24110  istdrg2  24122  isms2  24394  metuel2  24509  restmetu  24514  isngp  24540  isngp2  24541  isngp3  24542  elii1  24887  isncvsngp  25105  iscph  25126  isbn  25294  pmltpc  25407  ovolfcl  25423  finiunmbl  25501  iundisj  25505  dyaddisj  25553  vitalilem1  25565  ellimc3  25836  ig1pval3  26139  plyun0  26158  plydivex  26261  aannenlem2  26293  ellogrn  26524  atandm  26842  atandm3  26844  atans2  26897  elno3  27623  conway  27775  eqcuts2  27782  madeval2  27829  ons2ind  28271  tgjustf  28545  colinearalg  28983  axeuclid  29036  nbgrsym  29436  upgrtrls  29773  upgristrl  29774  dfpth2  29802  usgr2pth0  29838  iswwlks  29909  isclwwlk  30059  clwwlkneq0  30104  h2hlm  31055  issh  31283  chcon2i  31539  chcon1i  31540  chcon3i  31541  chnlei  31560  cmcm2i  31668  cmcm3i  31669  3oalem3  31739  pjdifnormii  31758  pjneli  31798  dfadj2  31960  cnvadj  31967  hhcno  31979  hhcnf  31980  eleigvec  32032  eleigvec2  32033  pjimai  32251  isst  32288  ishst  32289  cvnbtwn4  32364  chrelat4i  32448  2reucom  32554  reuxfrdf  32565  difrab2  32572  inpr0  32607  iunin1f  32632  disjnf  32645  cbvdisjf  32646  disjorf  32654  iundisjf  32664  disjexc  32668  xrdifh  32860  iundisjfi  32876  hashxpe  32887  pmtrprfv2  33170  xrnarchi  33266  isunit2  33322  prmidl0  33531  opprnsg  33565  ccfldextdgrr  33829  cmpcref  34007  ordtconnlem1  34081  isrrext  34157  cntnevol  34385  ddemeas  34393  omssubaddlem  34456  omssubadd  34457  eulerpartleme  34520  eulerpartlemv  34521  eulerpartlemt0  34526  eulerpartlemgvv  34533  eulerpartlemn  34538  ballotlem2  34646  ballotlemodife  34655  oddprm2  34812  bnj257  34863  bnj268  34865  bnj290  34866  bnj312  34868  bnj89  34877  bnj887  34921  bnj976  34933  bnj1019  34935  bnj1146  34947  bnj1385  34988  bnj110  35014  bnj121  35026  bnj130  35030  bnj153  35036  bnj543  35049  bnj580  35069  bnj607  35072  bnj849  35081  bnj882  35082  bnj916  35089  bnj985v  35109  bnj985  35110  bnj1033  35125  bnj1083  35134  bnj1090  35135  bnj1128  35146  bnj1174  35159  bnj1228  35167  onvf1odlem1  35297  erdszelem1  35385  cvmliftlem15  35492  snmlval  35525  satfvsuclem2  35554  satfdm  35563  elmpst  35730  mpstrcl  35735  orbi2iALT  35879  untuni  35903  dfso3  35914  xpab  35920  dftr6  35945  coep  35946  coepr  35947  dffr5  35948  dfso2  35949  cnvco1  35953  cnvco2  35954  eldm3  35955  dfdm5  35967  dfrn5  35968  brsset  36081  idsset  36082  dfon3  36084  dfbigcup2  36091  dfom5b  36104  dffun10  36106  dfiota3  36115  fnimage  36121  brdomain  36125  brrange  36126  brimg  36129  brapply  36130  brcup  36131  brcap  36132  lemsuccf  36133  funpartlem  36136  brrestrict  36143  dfrecs2  36144  brub  36148  altopelaltxp  36170  rmoeqi  36381  rmoeqbii  36382  reueqi  36383  reueqbii  36384  sbceqbii  36385  disjeq1i  36386  cbvralvw2  36420  cbvrexvw2  36421  cbvrmovw2  36422  cbvreuvw2  36423  cbvsbcvw2  36424  cbvdisjvw2  36429  trer  36510  filnetlem4  36575  df3nandALT1  36593  imnand2  36596  bj-dfbi5  36774  bj-bixor  36791  bj-nnfnt  36941  bj-csbsnlem  37104  bj-rcleqf  37226  bj-sscon  37230  bj-pw0ALT  37250  bj-restpw  37297  bj-opelidb1  37358  bj-imdiridlem  37390  bj-imdirco  37395  wl-df3xor2  37674  wl-3xorrot  37682  wl-3xorcoma  37683  wl-3xornot  37686  wl-df2-3mintru2  37690  wl-df3-3mintru2  37691  wl-df4-3mintru2  37692  wl-equsalvw  37743  wl-sb9v  37754  iundif1  37795  poimirlem25  37846  poimirlem26  37847  poimirlem30  37851  ismblfin  37862  mbfposadd  37868  itg2addnclem2  37873  ftc1anc  37902  inixp  37929  prdstotbnd  37995  heibor1lem  38010  isrngohom  38166  isidl  38215  isfldidl2  38270  isdmn3  38275  sbccom2lem  38325  triantru3  38432  vvdifopab  38458  brres2  38466  eldmqsres  38486  inxpss  38510  ref5  38512  n0el2  38528  dfsucmap3  38637  trcoss2  38747  dfeqvrel2  38847  dfeqvrel3  38848  redundeq1  38886  redundpbi1  38888  refrelredund4  38892  funALTVfun  38957  dfeldisj3  38978  dfeldisj5  38980  pet0  39074  petid  39076  petidres  39078  petinidres  39080  petxrnidres  39082  mpet  39098  petincnvepres  39108  pet  39110  pmapglbx  40029  lhpexle3  40272  cdleme25cv  40618  dicelval3  41440  diclspsn  41454  lcfls1c  41796  sn-axrep5v  42473  sn-iotalem  42477  psspwb  42484  redvmptabs  42615  eu6w  42919  moxfr  42934  fphpd  43058  uniel  43459  dflim6  43506  onsucf1olem  43512  dflim7  43515  omge2  43540  oenassex  43560  safesnsupfilb  43659  ifpim1  43710  ifpnot  43711  ifpid2  43712  ifpim2  43713  ifpxorcor  43717  ifpnot23  43719  ifpananb  43747  ifpnannanb  43748  ifpxorxorb  43752  rp-fakeinunass  43756  snen1g  43765  pren2  43794  alephiso2  43799  undmrnresiss  43845  cnvssco  43847  cotrintab  43855  cnviun  43891  imaiun1  43892  coiun1  43893  elintima  43894  frege133d  44006  frege54cor0a  44104  or3or  44264  andi3or  44265  ntrneik4w  44341  k0004lem1  44388  ismnuprim  44535  ismnushort  44542  undisjrab  44547  nzss  44558  pm10.541  44608  compab  44682  onfrALTlem5  44783  onfrALTlem5VD  45125  rext0  45179  wfaxun  45240  brpermmodel  45244  permaxrep  45247  permaxpow  45250  permac8prim  45255  eluni2f  45347  euabsneu  47274  aiotaexb  47335  aiotavb  47336  r19.32  47344  3an4ancom24  47515  ichn  47702  ichcom  47705  ichbi12i  47706  prproropf1olem0  47748  pairreueq  47756  clnbgrsym  48084  usgrexmpl2nb0  48277  usgrexmpl2nb1  48278  usgrexmpl2nb2  48279  usgrexmpl2nb3  48280  usgrexmpl2nb4  48281  usgrexmpl2nb5  48282  sgrp2sgrp  48474  islindeps  48699  elbigo  48797  reutruALT  49050  coxp  49078  tposres0  49122  catcinv  49644  isthincd2  49682  setrec1lem3  49934  elpg  49959