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  649  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  1429  an6  1448  3or6  1450  an3andi  1485  an33rean  1486  nancom  1498  xorass  1517  anxordi  1528  norass  1539  hadbi  1600  hadcoma  1601  hadcomb  1602  hadnot  1604  cador  1610  cadan  1611  cadcoma  1614  cadnot  1617  nic-axALT  1676  19.26-3an  1874  19.43OLD  1885  19.32v  1942  19.31v  1943  19.42v  1955  4exdistr  1963  cbvexvw  2039  exexw  2055  sb3an  2087  sbcom4  2095  sbbiiev  2098  excom  2168  sbal  2175  19.32  2241  19.31  2242  19.42  2244  equsalv  2275  sbex  2288  sbrim  2311  sbor  2313  sbbi  2314  sbnfOLD  2319  cbvex2v  2349  eeeanv  2355  sbnf2  2363  cbvsbvf  2368  cbvex2  2417  equsal  2422  dfsb3  2499  mo4  2567  eu6  2575  dfeu  2596  sb8eulem  2599  sb8mo  2602  cbvmovw  2603  cbvmow  2604  cbveuvw  2606  cbveuw  2607  cbveuALT  2609  eu1  2611  sbmo  2615  cbvabv  2807  cbvabw  2808  cbvab  2809  eqabcbw  2811  eqabcb  2877  nfceqi  2896  ralbii2  3080  rexbii2  3081  r19.26-3  3099  r19.43  3106  r2allem  3126  r19.42v  3170  r19.32v  3171  reeanlem  3209  3reeanv  3211  cbvralvw  3216  cbvrexvw  3217  ralcom  3266  ralcomf  3276  rexcomf  3277  cbvralfw  3278  cbvralsvw  3289  cbvralf  3332  cbvrexf  3333  reu5  3354  rmobiia  3358  reubiia  3359  rmo5  3370  cbvrmovw  3373  cbvreuvw  3374  cbvrmow  3377  cbvreuw  3378  cbvreu  3393  cbvrmo  3394  rabid2f  3432  abv  3454  abvALT  3455  ceqsal  3480  ceqsalv  3482  cgsex4gOLD  3490  ceqsex3v  3497  ceqsex4v  3498  ceqsex8v  3500  reurab  3661  eueq  3668  reu2  3685  reu6  3686  reu3  3687  rmo4  3690  rmo3f  3694  2reu5  3718  cbvsbcw  3775  cbvsbcvw  3776  cbvsbc  3777  sbc3an  3807  sbccomlemOLD  3822  rmo3  3841  rmoanim  3846  rmoanimALT  3847  cbvralcsf  3893  cbvrexcsf  3894  cbvreucsf  3895  eqss  3951  uniiunlem  4041  sspsstri  4059  compleq  4106  ssequn1  4140  unss  4144  rexun  4150  ralunb  4151  elin3  4160  inass  4182  ssin  4193  elsymdif  4212  nssinpss  4221  dfun2  4224  difin  4226  indi  4238  indifdi  4248  difin2  4255  eq0  4304  ssdif0  4320  inn0f  4325  inssdif0  4328  ab0w  4333  ab0  4334  ab0orv  4337  abn0  4339  rabeq0w  4341  rabeq0  4342  disj3  4408  ssundif  4442  ralidmw  4471  dfif2  4483  eldifpr  4617  rexdifpr  4618  rexsns  4630  snprc  4676  reusn  4686  difsnpss  4765  tpss  4795  pwpr  4859  eluni2  4869  elunirab  4880  uniun  4888  unissb  4898  elintrab  4917  ssintrab  4928  intun  4937  iuncom  4956  iuncom4  4957  iunab  5009  ssiinf  5012  iunn0  5024  iinab  5025  iunin2  5028  iinun2  5030  iundif2  5031  iunun  5050  iunxun  5051  iunxiun  5054  sspwuni  5057  iinpw  5063  cbvdisj  5077  cbvdisjv  5078  disjor  5082  brun  5151  brin  5152  brdif  5153  dftr2  5209  dftr5  5211  intexrab  5294  inuni  5297  ssext  5409  pweqb  5411  otth2  5439  otthne  5442  propeqop  5463  vopelopabsb  5485  eqopab2bw  5504  eqopab2b  5508  pwin  5523  pwun  5525  dffr6  5588  elxp2  5656  otelxp  5676  xpiundi  5703  xpiundir  5704  poinxp  5713  soinxp  5714  frinxp  5715  seinxp  5716  weinxp  5717  reliun  5773  inopab  5786  difopab  5787  inxp  5788  raliunxp  5796  rexiunxp  5797  rexxpf  5804  iunxpf  5805  cnvco  5842  dmiun  5870  dmuni  5871  dm0rn0  5881  dm0rn0OLD  5882  dmres  5979  restidsing  6020  asymref  6081  codir  6085  qfto  6086  cnvopab  6102  cnvopabOLD  6103  cnvdif  6109  rniun  6113  dminss  6119  imainss  6120  difxp  6130  xpdifid  6134  dmsnn0  6173  cnvcnvsn  6185  cnvresima  6196  resco  6216  imaco  6217  rnco  6218  rncoOLD  6219  coiun  6223  coass  6232  ressn  6251  cnviin  6252  cnvpo  6253  cnvso  6254  xpco  6255  opreu2reurex  6260  dfpo2  6262  imaindm  6265  dflim2  6383  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  7090  imaiun  7201  isocnv2  7287  isocnv3  7288  isores2  7289  isomin  7293  eqoprab2bw  7438  eqoprab2b  7439  elpwpwel  7722  sucexb  7759  onsucb  7769  dflim4  7800  fiun  7897  f1iun  7898  f11o  7901  opabex3d  7919  opabex3rd  7920  opabex3  7921  dfopab2  8006  dfoprab3s  8007  fmpox  8021  fparlem1  8064  fparlem2  8065  tpostpos  8198  frrlem9  8246  dfsmo2  8289  brwitnlem  8444  oarec  8499  naddasslem1  8632  naddasslem2  8633  qsid  8730  uniinqs  8746  mapval2  8822  mapsncnv  8843  elixp2  8851  ixpin  8873  brsdom  8923  brdom2  8931  xpassen  9011  brsdom2  9041  unfilem1  9217  fiint  9239  dfsup2  9359  supmo  9367  eqinf  9400  infmo  9412  brttrcl2  9635  rankc1  9794  cp  9815  isinfcard  10014  aceq1  10039  aceq2  10041  dfac5lem3  10047  dfac10b  10062  dfac12a  10071  dffin7-2  10320  dfacfin7  10321  fin1a2lem6  10327  iunfo  10461  konigthlem  10491  axgroth6  10751  axgroth3  10754  sstskm  10765  ltexprlem1  10959  gt0srpr  11001  ltpsrpr  11032  map2psrpr  11033  ltresr  11063  fimaxre3  12100  sup3  12111  supaddc  12121  supmul1  12123  elnn0z  12513  elznn0nn  12514  zmin  12869  xrnemnf  13043  xrnepnf  13044  dfrp2  13322  elioomnf  13372  elxrge0  13385  elfzuzb  13446  fzass4  13490  elfz2nn0  13546  elfzo2  13590  elfzo3  13604  lbfzo0  13627  fzo1lb  13641  fzind2  13716  nn0opthlem1  14203  hashgt23el  14359  cotr2g  14911  rexfiuz  15283  fsumcom2  15709  prodmo  15871  fprodcom2  15919  sinltx  16126  divalglem4  16335  divalglem10  16341  4sqlem12  16896  imasleval  17474  xpsfrnel  17495  xpscf  17498  isssc  17756  isffth2  17854  ispos2  18250  issubmgm  18639  ismhm  18722  issubmndb  18742  nsgacs  19103  isgim  19203  oppgcntz  19305  f1omvdco3  19390  pmtrprfvalrn  19429  efgrelexlemb  19691  pgpfac1  20023  pgpfac  20027  issrg  20135  opprsubg  20300  opprunit  20325  isirred2  20369  opprirred  20370  opprnzrb  20466  isdomn2OLD  20657  opprdomnb  20662  isdomn4r  20664  drngprop  20689  opprdrng  20709  issdrg2  20740  isorng  20806  islss  20897  islbs  21040  unocv  21647  iunocv  21648  isbasis2g  22904  tgval2  22912  ntreq0  23033  isclo2  23044  cmpcov2  23346  is1stc2  23398  1stcelcls  23417  llyi  23430  unisngl  23483  txuni2  23521  xkobval  23542  hausdiag  23601  isfbas2  23791  elfg  23827  fbasrn  23840  fmfnfmlem3  23912  isfcls  23965  alexsubALTlem2  24004  istmd  24030  istgp  24033  istrg  24120  istdrg  24122  istdrg2  24134  isms2  24406  metuel2  24521  restmetu  24526  isngp  24552  isngp2  24553  isngp3  24554  elii1  24899  isncvsngp  25117  iscph  25138  isbn  25306  pmltpc  25419  ovolfcl  25435  finiunmbl  25513  iundisj  25517  dyaddisj  25565  vitalilem1  25577  ellimc3  25848  ig1pval3  26151  plyun0  26170  plydivex  26273  aannenlem2  26305  ellogrn  26536  atandm  26854  atandm3  26856  atans2  26909  elno3  27635  conway  27787  eqcuts2  27794  madeval2  27841  ons2ind  28283  tgjustf  28557  colinearalg  28995  axeuclid  29048  nbgrsym  29448  upgrtrls  29785  upgristrl  29786  dfpth2  29814  usgr2pth0  29850  iswwlks  29921  isclwwlk  30071  clwwlkneq0  30116  h2hlm  31068  issh  31296  chcon2i  31552  chcon1i  31553  chcon3i  31554  chnlei  31573  cmcm2i  31681  cmcm3i  31682  3oalem3  31752  pjdifnormii  31771  pjneli  31811  dfadj2  31973  cnvadj  31980  hhcno  31992  hhcnf  31993  eleigvec  32045  eleigvec2  32046  pjimai  32264  isst  32301  ishst  32302  cvnbtwn4  32377  chrelat4i  32461  2reucom  32566  reuxfrdf  32577  difrab2  32584  inpr0  32619  iunin1f  32644  disjnf  32657  cbvdisjf  32658  disjorf  32666  iundisjf  32676  disjexc  32680  xrdifh  32871  iundisjfi  32887  hashxpe  32898  pmtrprfv2  33182  xrnarchi  33278  isunit2  33334  prmidl0  33543  opprnsg  33577  ccfldextdgrr  33850  cmpcref  34028  ordtconnlem1  34102  isrrext  34178  cntnevol  34406  ddemeas  34414  omssubaddlem  34477  omssubadd  34478  eulerpartleme  34541  eulerpartlemv  34542  eulerpartlemt0  34547  eulerpartlemgvv  34554  eulerpartlemn  34559  ballotlem2  34667  ballotlemodife  34676  oddprm2  34833  bnj257  34884  bnj268  34886  bnj290  34887  bnj312  34889  bnj89  34898  bnj887  34942  bnj976  34954  bnj1019  34956  bnj1146  34967  bnj1385  35008  bnj110  35034  bnj121  35046  bnj130  35050  bnj153  35056  bnj543  35069  bnj580  35089  bnj607  35092  bnj849  35101  bnj882  35102  bnj916  35109  bnj985v  35129  bnj985  35130  bnj1033  35145  bnj1083  35154  bnj1090  35155  bnj1128  35166  bnj1174  35179  bnj1228  35187  onvf1odlem1  35319  erdszelem1  35407  cvmliftlem15  35514  snmlval  35547  satfvsuclem2  35576  satfdm  35585  elmpst  35752  mpstrcl  35757  orbi2iALT  35901  untuni  35925  dfso3  35936  xpab  35942  dftr6  35967  coep  35968  coepr  35969  dffr5  35970  dfso2  35971  cnvco1  35975  cnvco2  35976  eldm3  35977  dfdm5  35989  dfrn5  35990  brsset  36103  idsset  36104  dfon3  36106  dfbigcup2  36113  dfom5b  36126  dffun10  36128  dfiota3  36137  fnimage  36143  brdomain  36147  brrange  36148  brimg  36151  brapply  36152  brcup  36153  brcap  36154  lemsuccf  36155  funpartlem  36158  brrestrict  36165  dfrecs2  36166  brub  36170  altopelaltxp  36192  rmoeqi  36403  rmoeqbii  36404  reueqi  36405  reueqbii  36406  sbceqbii  36407  disjeq1i  36408  cbvralvw2  36442  cbvrexvw2  36443  cbvrmovw2  36444  cbvreuvw2  36445  cbvsbcvw2  36446  cbvdisjvw2  36451  trer  36532  filnetlem4  36597  df3nandALT1  36615  imnand2  36618  bj-dfbi5  36799  bj-bixor  36816  bj-nnfnt  36993  bj-csbsnlem  37151  bj-rcleqf  37273  bj-sscon  37277  bj-pw0ALT  37297  bj-restpw  37345  bj-opelidb1  37408  bj-imdiridlem  37440  bj-imdirco  37445  wl-df3xor2  37724  wl-3xorrot  37732  wl-3xorcoma  37733  wl-3xornot  37736  wl-df2-3mintru2  37740  wl-df3-3mintru2  37741  wl-df4-3mintru2  37742  wl-equsalvw  37793  wl-sb9v  37804  iundif1  37845  poimirlem25  37896  poimirlem26  37897  poimirlem30  37901  ismblfin  37912  mbfposadd  37918  itg2addnclem2  37923  ftc1anc  37952  inixp  37979  prdstotbnd  38045  heibor1lem  38060  isrngohom  38216  isidl  38265  isfldidl2  38320  isdmn3  38325  sbccom2lem  38375  triantru3  38487  vvdifopab  38516  brres2  38524  eldmqsres  38544  inxpss  38568  ref5  38570  n0el2  38586  dfsucmap3  38714  trcoss2  38825  dfeqvrel2  38925  dfeqvrel3  38926  redundeq1  38964  redundpbi1  38966  refrelredund4  38970  funALTVfun  39034  dfeldisj3  39062  dfeldisj5  39064  pet0  39169  petid  39171  petidres  39173  petinidres  39175  petxrnidres  39177  mpet  39204  petincnvepres  39214  pet  39216  pmapglbx  40145  lhpexle3  40388  cdleme25cv  40734  dicelval3  41556  diclspsn  41570  lcfls1c  41912  sn-axrep5v  42589  sn-iotalem  42593  psspwb  42600  redvmptabs  42730  eu6w  43034  moxfr  43049  fphpd  43173  uniel  43574  dflim6  43621  onsucf1olem  43627  dflim7  43630  omge2  43655  oenassex  43675  safesnsupfilb  43774  ifpim1  43825  ifpnot  43826  ifpid2  43827  ifpim2  43828  ifpxorcor  43832  ifpnot23  43834  ifpananb  43862  ifpnannanb  43863  ifpxorxorb  43867  rp-fakeinunass  43871  snen1g  43880  pren2  43909  alephiso2  43914  undmrnresiss  43960  cnvssco  43962  cotrintab  43970  cnviun  44006  imaiun1  44007  coiun1  44008  elintima  44009  frege133d  44121  frege54cor0a  44219  or3or  44379  andi3or  44380  ntrneik4w  44456  k0004lem1  44503  ismnuprim  44650  ismnushort  44657  undisjrab  44662  nzss  44673  pm10.541  44723  compab  44797  onfrALTlem5  44898  onfrALTlem5VD  45240  rext0  45294  wfaxun  45355  brpermmodel  45359  permaxrep  45362  permaxpow  45365  permac8prim  45370  eluni2f  45462  euabsneu  47388  aiotaexb  47449  aiotavb  47450  r19.32  47458  3an4ancom24  47629  ichn  47816  ichcom  47819  ichbi12i  47820  prproropf1olem0  47862  pairreueq  47870  clnbgrsym  48198  usgrexmpl2nb0  48391  usgrexmpl2nb1  48392  usgrexmpl2nb2  48393  usgrexmpl2nb3  48394  usgrexmpl2nb4  48395  usgrexmpl2nb5  48396  sgrp2sgrp  48588  islindeps  48813  elbigo  48911  reutruALT  49164  coxp  49192  tposres0  49236  catcinv  49758  isthincd2  49796  setrec1lem3  50048  elpg  50073