Theorem 3bitr4i 306

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 281	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitri 278	1 ⊢ (𝜒 ↔ 𝜃)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi2d  345  pm4.71  567  pm5.32ri  586  an31  661  pm4.14  819  or4  940  orimdi  944  orbidi  967  ordi  1023  ordir  1024  andir  1026  dfbi3  1065  dfifp7  1085  ifpdfbiOLD  1087  ifpn  1090  3orrot  1108  3orcoma  1109  3ioran  1123  3ianor  1124  3anbi123i  1173  3orbi123i  1174  3jaob  1453  an6  1474  3or6  1476  an3andi  1513  an33rean  1514  nancom  1525  xorass  1544  anxordi  1555  norass  1566  hadbi  1627  hadcoma  1628  hadcomb  1629  hadnot  1631  cador  1640  cadan  1641  cadcoma  1644  cadnot  1647  nic-axALT  1706  19.26-3an  1904  19.43OLD  1915  19.32v  1972  19.31v  1973  19.42v  1985  4exdistr  1993  cbvexvw  2069  exexw  2085  sb3an  2117  sbcom4  2125  sbbiiev  2129  excom  2198  sbal  2205  19.32  2269  19.31  2270  19.42  2272  equsalv  2301  sbex  2314  sbrim  2337  sbor  2339  sbbi  2340  cbvex2v  2373  eeeanv  2379  sbnf2  2387  cbvsbvf  2392  cbvex2  2441  equsal  2446  dfsb3  2523  mo4  2591  eu6  2599  dfeu  2620  sb8eulem  2623  sb8mo  2626  cbvmovw  2627  cbvmow  2628  cbveuvw  2630  cbveuw  2631  cbveuALT  2633  eu1  2635  sbmo  2639  cbvabv  2830  cbvabw  2831  cbvab  2832  eqabcbw  2834  eqabcb  2900  nfceqi  2919  ralbii2  3104  rexbii2  3105  r19.26-3  3123  r19.43  3130  r2allem  3150  r19.42v  3194  r19.32v  3195  reeanlem  3233  3reeanv  3235  cbvralvw  3240  cbvrexvw  3241  ralcom  3290  ralcomf  3300  rexcomf  3301  cbvralfw  3302  cbvralsvw  3313  cbvralf  3345  cbvrexf  3346  reu5  3367  rmobiia  3371  reubiia  3372  rmo5  3383  cbvrmovw  3386  cbvreuvw  3387  cbvrmow  3390  cbvreuw  3391  cbvreu  3404  cbvrmo  3405  rabid2f  3442  abv  3462  abvALT  3463  ceqsal  3487  ceqsalv  3489  ceqsex3v  3502  ceqsex4v  3503  ceqsex8v  3505  reurab  3658  eueq  3665  reu2  3682  reu6  3683  reu3  3684  rmo4  3687  rmo3f  3691  2reu5  3715  cbvsbcw  3771  cbvsbcvw  3772  cbvsbc  3773  sbc3an  3802  rmo3  3836  rmoanim  3842  rmoanimALT  3843  cbvralcsf  3889  cbvrexcsf  3890  cbvreucsf  3891  eqss  3924  uniiunlem  4011  sspsstri  4032  compleq  4087  elin3  4102  inass  4123  ssin  4134  ssequn1  4183  unss  4187  rexun  4193  ralunb  4194  elsymdif  4202  nssinpss  4211  dfun2  4214  difin  4216  indi  4228  indifdi  4238  difin2  4245  eq0  4296  ssdif0  4313  inn0f  4318  inssdif0OLD  4322  ab0w  4327  ab0  4328  ab0orv  4331  abn0  4333  rabeq0w  4336  rabeq0  4337  disj3  4406  ssundif  4442  ralidmw  4471  dfif2  4483  eldifpr  4615  rexdifpr  4616  rexsns  4628  snprc  4674  reusn  4684  difsnpss  4766  tpss  4791  pwpr  4827  eluni2  4870  elunirab  4881  uniun  4889  unissb  4900  elintrab  4919  ssintrab  4930  intun  4939  iuncom  4958  iuncom4  4959  iunab  5009  ssiinf  5012  iunn0  5024  iinab  5025  iunin2  5028  iinun2  5030  iundif2  5031  iunun  5052  iunxun  5053  iunxiun  5056  sspwuni  5059  iinpw  5065  cbvdisj  5079  cbvdisjv  5080  disjor  5084  brun  5155  brin  5156  brdif  5157  dftr2  5213  dftr5  5215  intexrab  5308  inuni  5311  ssext  5422  pweqb  5424  otth2  5452  otthne  5455  propeqop  5479  vopelopabsb  5503  eqopab2bw  5523  eqopab2b  5527  pwin  5542  pwun  5544  dffr6  5607  elxp2  5675  otelxp  5695  xpiundi  5722  xpiundir  5723  poinxp  5733  soinxp  5734  frinxp  5735  seinxp  5736  weinxp  5737  reliun  5795  inopab  5808  difopab  5809  inxp  5810  raliunxp  5817  rexiunxp  5818  rexxpf  5826  iunxpf  5827  cnvco  5868  dmiun  5896  dmuni  5897  dm0rn0  5907  dm0rn0OLD  5908  dmres  6005  restidsing  6047  asymref  6112  codir  6116  qfto  6117  cnvopab  6133  cnvdif  6136  rniun  6141  dminss  6145  imainss  6146  cnvxp  6149  difxp  6157  xpdifid  6161  xpdifcnvepel  6162  dmsnn0  6211  cnvcnvsn  6223  cnvresima  6234  resco  6254  imaco  6255  rnco  6256  rncoOLD  6257  coiun  6261  coass  6270  ressn  6291  cnviin  6292  cnvpo  6293  cnvso  6294  xpco  6295  opreu2reurex  6300  dfpo2  6302  imaindm  6305  dflim2  6424  funcnv  6614  funcnv3  6615  fncnv  6618  fun11  6619  imadif  6629  fnres  6671  dfmpt3  6678  mptfnf  6679  fnopabg  6681  fint  6766  fin  6767  fores  6811  dff1o3  6836  f1ompt  7116  fsn  7141  imaiun  7253  isocnv2  7343  isocnv3  7344  isores2  7345  isomin  7349  eqoprab2bw  7494  eqoprab2b  7495  elpwpwel  7785  sucexb  7822  onsucb  7832  dflim4  7863  fiun  7959  f1iun  7960  f11o  7963  opabex3d  7981  opabex3rd  7982  opabex3  7983  dfopab2  8068  dfoprab3s  8069  fmpox  8083  fparlem1  8130  fparlem2  8131  suppvalbr  8188  tpostpos  8271  frrlem9  8320  dfsmo2  8363  brwitnlem  8523  oarec  8578  naddasslem1  8712  naddasslem2  8713  qsid  8810  uniinqs  8826  mapval2  8908  mapsncnv  8929  elixp2  8937  ixpin  8959  brsdom  9009  brdom2  9017  xpassen  9098  brsdom2  9128  unfilem1  9305  fiint  9326  dfsup2  9443  supmo  9451  eqinf  9484  infmo  9496  brttrcl2  9722  rankc1  9894  cp  9961  setrec1lem3  9976  isinfcard  10178  aceq1  10203  aceq2  10205  dfac5lem3  10211  dfac10b  10225  dfac12a  10234  dffin7-2  10483  dfacfin7  10484  fin1a2lem6  10490  iunfo  10630  konigthlem  10660  axgroth6  10920  axgroth3  10923  sstskm  10934  ltexprlem1  11128  gt0srpr  11170  ltpsrpr  11201  map2psrpr  11202  ltresr  11232  fimaxre3  12270  sup3  12281  supaddc  12291  supmul1  12293  elnn0z  12713  elznn0nn  12714  zmin  13078  xrnemnf  13253  xrnepnf  13254  dfrp2  13532  elioomnf  13582  elxrge0  13595  elfzuzb  13657  fzass4  13703  elfz2nn0  13759  elfzo2  13803  elfzo3  13818  lbfzo0  13841  fzo1lb  13855  fzind2  13930  nn0opthlem1  14419  hashgt23el  14576  cotr2g  15138  rexfiuz  15524  fsumcom2  15949  prodmo  16112  fprodcom2  16160  sinltx  16366  divalglem4  16575  divalglem10  16581  4sqlem12  17143  imasleval  17722  xpsfrnel  17743  xpscf  17746  isssc  18004  isffth2  18102  ispos2  18498  issubmgm  18900  ismhm  18989  issubmndb  19009  nsgacs  19381  isgim  19485  oppgcntz  19587  f1omvdco3  19672  pmtrprfvalrn  19711  efgrelexlemb  19973  pgpfac1  20305  pgpfac  20309  issrg  20423  dfring3  20527  opprsubg  20591  opprunit  20616  isirred2  20660  opprirred  20661  isrhm0  20715  dfric2  20766  opprnzrb  20781  opprdomnb  20977  isdomn4r  20979  drngprop  21007  isdrng3  21016  isdrng5  21017  opprdrng  21030  issdrg2  21061  isorng  21127  islss  21218  islbs  21360  isfieldidl  21549  isfieldidl2  21550  prmidl0  21643  unocv  21995  iunocv  21996  isbasis2g  23275  tgval2  23283  ntreq0  23404  isclo2  23415  cmpcov2  23717  is1stc2  23769  1stcelcls  23789  llyi  23802  unisngl  23855  txuni2  23893  xkobval  23914  hausdiag  23973  isfbas2  24163  elfg  24199  fbasrn  24212  fmfnfmlem3  24284  isfcls  24337  alexsubALTlem2  24376  istmd  24402  istgp  24405  istrg  24492  istdrg  24494  istdrg2  24506  isms2  24778  metuel2  24893  restmetu  24898  isngp  24924  isngp2  24925  isngp3  24926  elii1  25265  isncvsngp  25479  iscph  25500  isbn  25668  pmltpc  25780  ovolfcl  25796  finiunmbl  25874  iundisj  25878  dyaddisj  25926  vitalilem1  25938  ellimc3  26208  ig1pval3  26505  plyun0  26524  plydivex  26627  aannenlem2  26665  ellogrn  26896  atandm  27213  atandm3  27215  atans2  27268  elno3  28021  conway  28174  eqcuts2  28181  madeval2  28228  ons2ind  28670  tgjustf  28944  colinearalg  29497  axeuclid  29550  nbgrsym  29953  upgrtrls  30293  upgristrl  30294  dfpth2  30323  usgr2pth0  30360  iswwlks  30434  isclwwlk  30584  clwwlkneq0  30629  h2hlm  31591  issh  31819  chcon2i  32075  chcon1i  32076  chcon3i  32077  chnlei  32096  cmcm2i  32204  cmcm3i  32205  3oalem3  32275  pjdifnormii  32294  pjneli  32334  dfadj2  32496  cnvadj  32503  hhcno  32515  hhcnf  32516  eleigvec  32568  eleigvec2  32569  pjimai  32787  isst  32824  ishst  32825  cvnbtwn4  32900  chrelat4i  32984  2reucom  33127  reuxfrdf  33138  difrab2  33145  inpr0  33179  iunin1f  33203  disjnf  33215  cbvdisjf  33216  disjorf  33224  iundisjf  33234  disjexc  33238  xrdifh  33422  iundisjfi  33438  hashxpe  33449  pmtrprfv2  33699  xrnarchi  33795  isunit2  33850  opprnsg  34058  ccfldextdgrr  34354  cmpcref  34532  ordtconnlem1  34606  isrrext  34682  cntnevol  34911  ddemeas  34919  omssubaddlem  34981  omssubadd  34982  eulerpartleme  35045  eulerpartlemv  35046  eulerpartlemt0  35051  eulerpartlemgvv  35058  eulerpartlemn  35063  ballotlem2  35171  ballotlemodife  35180  oddprm2  35334  bnj257  35388  bnj268  35390  bnj290  35391  bnj312  35393  bnj89  35402  bnj887  35446  bnj976  35458  bnj1019  35460  bnj1146  35471  bnj1385  35512  bnj110  35538  bnj121  35550  bnj130  35554  bnj153  35560  bnj543  35573  bnj580  35593  bnj607  35596  bnj849  35605  bnj882  35606  bnj916  35613  bnj985v  35633  bnj985  35634  bnj1033  35649  bnj1083  35658  bnj1090  35659  bnj1128  35670  bnj1174  35683  bnj1228  35691  reu6f  35759  fwfffun  35767  fwfffunres  35768  0elscott  35813  onvf1odlem1  35982  srepdflem1  36036  srepdflem2  36037  erdszelem1  36074  cvmliftlem15  36181  snmlval  36214  satfvsuclem2  36243  satfdm  36252  elmpst  36419  mpstrcl  36424  orbi2iALT  36568  untuni  36598  dfso3  36609  xpab  36615  dftr6  36640  coep  36641  coepr  36642  dffr5  36643  dfso2  36644  cnvco1  36648  cnvco2  36649  eldm3  36650  dfdm5  36661  dfrn5  36662  brsset  36775  idsset  36776  dfon3  36778  dfbigcup2  36785  dfom5b  36798  dffun10  36800  dfiota3  36809  fnimage  36815  brdomain  36819  brrange  36820  brimg  36823  brapply  36824  brcup  36825  brcap  36826  lemsuccf  36827  funpartlem  36830  brrestrict  36837  dfrecs2  36838  brub  36842  dffr7  36844  altopelaltxp  36865  ltnadd  37091  rmoeqi  37100  rmoeqbii  37101  reueqi  37102  reueqbii  37103  sbceqbii  37104  disjeq1i  37105  cbvralvw2  37139  cbvrexvw2  37140  cbvrmovw2  37141  cbvreuvw2  37142  cbvsbcvw2  37143  cbvdisjvw2  37148  trer  37228  filnetlem4  37293  df3nandALT1  37311  imnand2  37314  mh-unprimbi  37456  bj-dfbi5  37568  bj-bixor  37585  bj-dfsbc  37675  bj-nnfnt  37776  bj-csbsnlem  37939  bj-rcleqf  38062  bj-sscon  38066  bj-dfres2  38086  bj-dfrel3  38089  bj-pw0ALT  38100  bj-restpw  38149  bj-opelidb1  38211  bj-imdiridlem  38243  bj-imdirco  38248  wl-df3xor2  38529  wl-3xorrot  38537  wl-3xorcoma  38538  wl-3xornot  38541  wl-df2-3mintru2  38545  wl-df3-3mintru2  38546  wl-df4-3mintru2  38547  wl-equsalvw  38607  wl-sb9v  38618  iundif1  38659  poimirlem25  38700  poimirlem26  38701  poimirlem30  38705  ismblfin  38716  mbfposadd  38722  itg2addnclem2  38727  ftc1anc  38756  inixp  38799  prdstotbnd  38865  heibor1lem  38880  isrngohom  39036  isidl  39085  isfldidl2  39140  isdmn3  39145  sbccom2lem  39193  scott0f  39238  triantru3  39305  vvdifopab  39334  brres2  39342  eldmqsres  39362  inxpss  39386  ref5  39388  n0el2  39404  dfsucmap3  39532  trcoss2  39643  dfeqvrel2  39743  dfeqvrel3  39744  redundeq1  39782  redundpbi1  39784  refrelredund4  39788  funALTVfun  39852  dfeldisj3  39880  dfeldisj5  39882  pet0  39987  petid  39989  petidres  39991  petinidres  39993  petxrnidres  39995  mpet  40022  petincnvepres  40032  pet  40034  pmapglbx  40963  lhpexle3  41206  cdleme25cv  41552  dicelval3  42374  diclspsn  42388  lcfls1c  42730  sn-axrep5v  43408  sn-iotalem  43412  psspwb  43419  redvmptabs  43548  eu6w  43824  moxfr  43840  fphpd  43960  uniel  44356  dflim6  44403  onsucf1olem  44409  dflim7  44412  omge2  44437  oenassex  44457  safesnsupfilb  44556  ifpim1  44607  ifpnot  44608  ifpid2  44609  ifpim2  44610  ifpxorcor  44614  ifpnot23  44616  ifpananb  44644  ifpnannanb  44645  ifpxorxorb  44649  rp-fakeinunass  44653  snen1g  44662  pren2  44691  alephiso2  44696  undmrnresiss  44741  cnvssco  44743  cotrintab  44751  cnviun  44787  imaiun1  44788  coiun1  44789  elintima  44790  frege133d  44902  frege54cor0a  45000  or3or  45160  andi3or  45161  ntrneik4w  45237  k0004lem1  45284  ismnuprim  45415  ismnushort  45422  undisjrab  45427  nzss  45438  pm10.541  45488  compab  45561  onfrALTlem5  45661  onfrALTlem5VD  46003  rext0  46057  wfaxun  46125  brpermmodel  46129  permaxrep  46132  permaxpow  46135  permac8prim  46140  eluni2f  46254  euabsneu  48234  aiotaexb  48295  aiotavb  48296  r19.32  48305  3an4ancom24  48475  ichn  48674  ichcom  48677  ichbi12i  48678  prproropf1olem0  48720  pairreueq  48728  clnbgrsym  49072  usgrexmpl2nb0  49265  usgrexmpl2nb1  49266  usgrexmpl2nb2  49267  usgrexmpl2nb3  49268  usgrexmpl2nb4  49269  usgrexmpl2nb5  49270  sgrp2sgrp  49461  isidom3  49578  islindeps  49701  elbigo  49799  reutruALT  50051  coxp  50080  tposres0  50126  isnat3  50478  catcinv  50670  isthincd2  50708  elpg  51018  dfrals2  51097  alsbii  51107  ralsbii  51108  cbvals  51112  dfralseu2  51130  alseubii  51139  ralseubii  51140