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  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  1154  3orbi123i  1155  3jaob  1425  an6  1444  3or6  1446  an3andi  1481  an33rean  1482  nancom  1492  xorass  1511  anxordi  1522  norass  1533  hadbi  1594  hadcoma  1595  hadcomb  1596  hadnot  1598  cador  1604  cadan  1605  cadcoma  1608  cadnot  1611  nic-axALT  1670  nfnbiOLD  1852  19.26-3an  1869  19.43OLD  1880  19.32v  1937  19.31v  1938  19.42v  1950  4exdistr  1958  cbvexvw  2033  exexw  2048  sb3an  2078  sbcom4  2086  sbbiiev  2089  excom  2159  sbal  2166  19.32  2230  19.31  2231  19.42  2233  equsalv  2264  sbex  2279  sbrim  2302  sbor  2305  sbbi  2306  sbnfOLD  2311  cbvex2v  2344  eeeanv  2350  sbnf2  2358  cbvsbvf  2363  cbvex2  2414  equsal  2419  dfsb3  2496  mo4  2563  eu6  2571  eubii  2582  dfeu  2592  sb8eulem  2595  sb8mo  2598  cbvmovw  2599  cbvmow  2600  cbveuvw  2602  cbveuw  2603  cbveuALT  2605  eu1  2607  sbmo  2611  cbvabv  2809  cbvabw  2810  cbvab  2811  eqabcb  2880  nfceqi  2899  sbabelOLD  2936  ralbii2  3086  rexbii2  3087  r19.26-3  3109  r19.43  3119  r2allem  3139  r19.21vOLD  3178  r19.42v  3188  r19.32v  3189  reeanlem  3225  3reeanv  3227  2ralorOLD  3229  cbvralvw  3234  cbvrexvw  3235  ralcom4OLD  3284  ralcom  3286  ralcomf  3299  rexcomf  3300  cbvralfw  3301  cbvralsvw  3314  cbvralf  3357  cbvrexf  3358  reu5  3379  rmobiia  3383  reubiia  3384  rmoanidOLD  3389  reuanidOLD  3390  rmo5  3397  cbvrmovw  3400  cbvreuvw  3401  moelOLD  3402  cbvrmow  3406  cbvreuw  3407  cbvreuwOLD  3412  cbvreu  3424  cbvrmo  3425  rabid2f  3465  rabid2OLD  3468  abv  3489  abvALT  3490  ceqsal  3516  ceqsalv  3518  cgsex4gOLD  3526  ceqsex3v  3536  ceqsex4v  3537  ceqsex8v  3539  reurab  3709  eueq  3716  reu2  3733  reu6  3734  reu3  3735  rmo4  3738  rmo3f  3742  2reu5  3766  cbvsbcw  3824  cbvsbcvw  3825  cbvsbc  3826  sbc3an  3860  sbccomlemOLD  3878  rmo3  3897  rmoanim  3902  rmoanimALT  3903  cbvralcsf  3952  cbvrexcsf  3953  cbvreucsf  3954  eqss  4010  uniiunlem  4096  sspsstri  4114  compleq  4161  ssequn1  4195  unss  4199  rexun  4205  ralunb  4206  elin3  4215  inass  4235  ssin  4246  elsymdif  4263  nssinpss  4272  dfun2  4275  difin  4277  indi  4289  indifdi  4299  difin2  4306  ssdif0  4371  inn0f  4376  inssdif0  4379  ab0  4385  abn0  4390  rabeq0w  4392  rabeq0  4393  disj  4455  disj3  4459  ssundif  4493  ralidmw  4513  dfif2  4532  eldifpr  4662  rexdifpr  4663  rexsns  4675  snprc  4721  reusn  4731  difsnpss  4811  tpss  4841  pwpr  4905  eluni2  4915  elunirab  4926  uniun  4934  unissb  4943  unissbOLD  4944  elintrab  4964  ssintrab  4975  intun  4984  iuncom  5003  iuncom4  5004  iunab  5055  ssiinf  5058  iunn0  5071  iinab  5072  iunin2  5075  iinun2  5077  iundif2  5078  iunun  5097  iunxun  5098  iunxiun  5101  sspwuni  5104  iinpw  5110  cbvdisj  5124  cbvdisjv  5125  disjor  5129  brun  5198  brin  5199  brdif  5200  dftr2  5266  dftr5  5268  intexrab  5352  inuni  5355  ssext  5464  pweqb  5466  otth2  5493  otthne  5496  propeqop  5516  vopelopabsb  5538  eqopab2bw  5557  eqopab2b  5561  pwin  5578  pwun  5580  dffr6  5643  elxp2  5712  otelxp  5732  xpiundi  5758  xpiundir  5759  poinxp  5768  soinxp  5769  frinxp  5770  seinxp  5771  weinxp  5772  inopab  5841  difopab  5842  difopabOLD  5843  inxp  5844  raliunxp  5852  rexiunxp  5853  rexxpf  5860  iunxpf  5861  cnvco  5898  dmiun  5926  dmuni  5927  dm0rn0  5937  dmres  6031  restidsing  6072  cnvsymOLDOLD  6136  asymref  6138  codir  6142  qfto  6143  cnvopab  6159  cnvopabOLD  6160  cnvdif  6165  rniun  6169  dminss  6174  imainss  6175  difxp  6185  xpdifid  6189  dmsnn0  6228  cnvcnvsn  6240  cnvresima  6251  resco  6271  imaco  6272  rnco  6273  coiun  6277  coass  6286  ressn  6306  cnviin  6307  cnvpo  6308  cnvso  6309  xpco  6310  opreu2reurex  6315  dfpo2  6317  imaindm  6320  dflim2  6442  funcnv  6636  funcnv3  6637  fncnv  6640  fun11  6641  imadif  6651  fnres  6695  dfmpt3  6702  mptfnf  6703  fnopabg  6705  fint  6787  fin  6788  fores  6830  dff1o3  6854  f1ompt  7130  fsn  7154  imaiun  7264  isocnv2  7350  isocnv3  7351  isores2  7352  isomin  7356  eqoprab2bw  7502  eqoprab2b  7503  elpwpwel  7785  sucexb  7823  onsucb  7836  dflim4  7868  fiun  7965  f1iun  7966  f11o  7969  opabex3d  7988  opabex3rd  7989  opabex3  7990  dfopab2  8075  dfoprab3s  8076  fmpox  8090  fparlem1  8135  fparlem2  8136  tpostpos  8269  frrlem9  8317  wfrlem8OLD  8354  wfrfunOLD  8357  dfsmo2  8385  brwitnlem  8543  oarec  8598  naddasslem1  8730  naddasslem2  8731  qsid  8821  uniinqs  8835  mapval2  8910  mapsncnv  8931  elixp2  8939  ixpin  8961  brsdom  9013  brdom2  9020  xpassen  9104  brsdom2  9135  dif1enOLD  9200  unfilem1  9340  fiint  9363  fiintOLD  9364  dfsup2  9481  supmo  9489  eqinf  9521  infmo  9532  brttrcl2  9751  rankc1  9907  cp  9928  isinfcard  10129  aceq1  10154  aceq2  10156  dfac5lem3  10162  dfac10b  10177  dfac12a  10186  dffin7-2  10435  dfacfin7  10436  fin1a2lem6  10442  iunfo  10576  konigthlem  10605  axgroth6  10865  axgroth3  10868  sstskm  10879  ltexprlem1  11073  gt0srpr  11115  ltpsrpr  11146  map2psrpr  11147  ltresr  11177  fimaxre3  12211  sup3  12222  supaddc  12232  supmul1  12234  elnn0z  12623  elznn0nn  12624  zmin  12983  xrnemnf  13156  xrnepnf  13157  dfrp2  13432  elioomnf  13480  elxrge0  13493  elfzuzb  13554  fzass4  13598  elfz2nn0  13654  elfzo2  13698  elfzo3  13712  lbfzo0  13735  fzo1lb  13749  fzind2  13820  nn0opthlem1  14303  hashgt23el  14459  cotr2g  15011  rexfiuz  15382  fsumcom2  15806  prodmo  15968  fprodcom2  16016  sinltx  16221  divalglem4  16429  divalglem10  16435  4sqlem12  16989  imasleval  17587  xpsfrnel  17608  xpscf  17611  isssc  17867  isffth2  17969  ispos2  18372  issubmgm  18727  ismhm  18810  issubmndb  18830  nsgacs  19192  isgim  19292  oppgcntz  19397  f1omvdco3  19481  pmtrprfvalrn  19520  efgrelexlemb  19782  pgpfac1  20114  pgpfac  20118  issrg  20205  opprsubg  20368  opprunit  20393  isirred2  20437  opprirred  20438  opprnzrb  20537  isdomn2OLD  20728  opprdomnb  20733  isdomn4r  20735  drngprop  20760  opprdrng  20780  issdrg2  20812  islss  20949  islbs  21092  unocv  21715  iunocv  21716  isbasis2g  22970  tgval2  22978  ntreq0  23100  isclo2  23111  cmpcov2  23413  is1stc2  23465  1stcelcls  23484  llyi  23497  unisngl  23550  txuni2  23588  xkobval  23609  hausdiag  23668  isfbas2  23858  elfg  23894  fbasrn  23907  fmfnfmlem3  23979  isfcls  24032  alexsubALTlem2  24071  istmd  24097  istgp  24100  istrg  24187  istdrg  24189  istdrg2  24201  isms2  24475  metuel2  24593  restmetu  24598  isngp  24624  isngp2  24625  isngp3  24626  elii1  24977  isncvsngp  25196  iscph  25217  isbn  25385  pmltpc  25498  ovolfcl  25514  finiunmbl  25592  iundisj  25596  dyaddisj  25644  vitalilem1  25656  ellimc3  25928  ig1pval3  26231  plyun0  26250  plydivex  26353  aannenlem2  26385  ellogrn  26615  atandm  26933  atandm3  26935  atans2  26988  elno3  27714  conway  27858  eqscut2  27865  madeval2  27906  tgjustf  28495  colinearalg  28939  axeuclid  28992  nbgrsym  29394  upgrtrls  29733  upgristrl  29734  usgr2pth0  29797  iswwlks  29865  isclwwlk  30012  clwwlkneq0  30057  h2hlm  31008  issh  31236  chcon2i  31492  chcon1i  31493  chcon3i  31494  chnlei  31513  cmcm2i  31621  cmcm3i  31622  3oalem3  31692  pjdifnormii  31711  pjneli  31751  dfadj2  31913  cnvadj  31920  hhcno  31932  hhcnf  31933  eleigvec  31985  eleigvec2  31986  pjimai  32204  isst  32241  ishst  32242  cvnbtwn4  32317  chrelat4i  32401  2reucom  32507  reuxfrdf  32518  difrab2  32525  inpr0  32557  iunin1f  32577  disjnf  32589  cbvdisjf  32590  disjorf  32598  iundisjf  32608  disjexc  32612  xrdifh  32788  iundisjfi  32803  hashxpe  32816  pmtrprfv2  33090  xrnarchi  33173  isunit2  33229  isorng  33308  prmidl0  33457  opprnsg  33491  ccfldextdgrr  33696  cmpcref  33810  ordtconnlem1  33884  isrrext  33962  cntnevol  34208  ddemeas  34216  omssubaddlem  34280  omssubadd  34281  eulerpartleme  34344  eulerpartlemv  34345  eulerpartlemt0  34350  eulerpartlemgvv  34357  eulerpartlemn  34362  ballotlem2  34469  ballotlemodife  34478  oddprm2  34648  bnj257  34699  bnj268  34701  bnj290  34702  bnj312  34704  bnj89  34713  bnj887  34757  bnj976  34769  bnj1019  34771  bnj1146  34783  bnj1385  34824  bnj110  34850  bnj121  34862  bnj130  34866  bnj153  34872  bnj543  34885  bnj580  34905  bnj607  34908  bnj849  34917  bnj882  34918  bnj916  34925  bnj985v  34945  bnj985  34946  bnj1033  34961  bnj1083  34970  bnj1090  34971  bnj1128  34982  bnj1174  34995  bnj1228  35003  erdszelem1  35175  cvmliftlem15  35282  snmlval  35315  satfvsuclem2  35344  satfdm  35353  elmpst  35520  mpstrcl  35525  orbi2iALT  35669  untuni  35688  dfso3  35699  xpab  35705  dftr6  35730  coep  35731  coepr  35732  dffr5  35733  dfso2  35734  cnvco1  35738  cnvco2  35739  eldm3  35740  dfdm5  35753  dfrn5  35754  brsset  35870  idsset  35871  dfon3  35873  dfbigcup2  35880  dfom5b  35893  dffun10  35895  dfiota3  35904  fnimage  35910  brdomain  35914  brrange  35915  brimg  35918  brapply  35919  brcup  35920  brcap  35921  brsuccf  35922  funpartlem  35923  brrestrict  35930  dfrecs2  35931  brub  35935  altopelaltxp  35957  rmoeqi  36168  rmoeqbii  36169  reueqi  36170  reueqbii  36171  sbceqbii  36172  disjeq1i  36173  cbvralvw2  36208  cbvrexvw2  36209  cbvrmovw2  36210  cbvreuvw2  36211  cbvsbcvw2  36212  cbvdisjvw2  36217  trer  36298  filnetlem4  36363  df3nandALT1  36381  imnand2  36384  bj-dfbi5  36556  bj-bixor  36573  bj-nnfnt  36722  bj-csbsnlem  36885  bj-rcleqf  37007  bj-sscon  37011  bj-pw0ALT  37031  bj-restpw  37074  bj-opelidb1  37135  bj-imdiridlem  37167  bj-imdirco  37172  wl-df3xor2  37451  wl-3xorrot  37459  wl-3xorcoma  37460  wl-3xornot  37463  wl-df2-3mintru2  37467  wl-df3-3mintru2  37468  wl-df4-3mintru2  37469  wl-equsalvw  37518  wl-sb9v  37529  iundif1  37580  poimirlem25  37631  poimirlem26  37632  poimirlem30  37636  ismblfin  37647  mbfposadd  37653  itg2addnclem2  37658  ftc1anc  37687  inixp  37714  prdstotbnd  37780  heibor1lem  37795  isrngohom  37951  isidl  38000  isfldidl2  38055  isdmn3  38060  sbccom2lem  38110  triantru3  38210  vvdifopab  38241  brres2  38249  eldmqsres  38268  inxpss  38292  ref5  38294  n0el2  38314  trcoss2  38465  dfeqvrel2  38571  dfeqvrel3  38572  redundeq1  38610  redundpbi1  38612  refrelredund4  38616  funALTVfun  38679  dfeldisj3  38700  dfeldisj5  38702  pet0  38796  petid  38798  petidres  38800  petinidres  38802  petxrnidres  38804  mpet  38820  petincnvepres  38830  pet  38832  pmapglbx  39751  lhpexle3  39994  cdleme25cv  40340  dicelval3  41162  diclspsn  41176  lcfls1c  41518  sn-axrep5v  42233  sn-iotalem  42238  psspwb  42245  redvmptabs  42368  eu6w  42662  moxfr  42679  fphpd  42803  uniel  43205  dflim6  43253  onsucf1olem  43259  dflim7  43262  omge2  43287  oenassex  43307  safesnsupfilb  43407  ifpim1  43458  ifpnot  43459  ifpid2  43460  ifpim2  43461  ifpxorcor  43465  ifpnot23  43467  ifpananb  43495  ifpnannanb  43496  ifpxorxorb  43500  rp-fakeinunass  43504  snen1g  43513  pren2  43542  alephiso2  43547  undmrnresiss  43593  cnvssco  43595  cotrintab  43603  cnviun  43639  imaiun1  43640  coiun1  43641  elintima  43642  frege133d  43754  frege54cor0a  43852  or3or  44012  andi3or  44013  ntrneik4w  44089  k0004lem1  44136  ismnuprim  44289  ismnushort  44296  undisjrab  44301  nzss  44312  pm10.541  44362  compab  44437  onfrALTlem5  44539  onfrALTlem5VD  44882  eluni2f  45042  euabsneu  46977  aiotaexb  47038  aiotavb  47039  r19.32  47047  3an4ancom24  47218  ichn  47380  ichcom  47383  ichbi12i  47384  prproropf1olem0  47426  pairreueq  47434  clnbgrsym  47761  usgrexmpl2nb0  47925  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  sgrp2sgrp  48071  islindeps  48298  elbigo  48400  reutruALT  48653  isthincd2  48837  setrec1lem3  48919  elpg  48944