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  3323  cbvrexf  3324  reu5  3345  rmobiia  3349  reubiia  3350  rmo5  3361  cbvrmovw  3364  cbvreuvw  3365  cbvrmow  3368  cbvreuw  3369  cbvreu  3382  cbvrmo  3383  rabid2f  3421  abv  3442  abvALT  3443  ceqsal  3468  ceqsalv  3470  ceqsex3v  3484  ceqsex4v  3485  ceqsex8v  3487  reurab  3648  eueq  3655  reu2  3672  reu6  3673  reu3  3674  rmo4  3677  rmo3f  3681  2reu5  3705  cbvsbcw  3762  cbvsbcvw  3763  cbvsbc  3764  sbc3an  3794  sbccomlemOLD  3809  rmo3  3828  rmoanim  3833  rmoanimALT  3834  cbvralcsf  3880  cbvrexcsf  3881  cbvreucsf  3882  eqss  3938  uniiunlem  4028  sspsstri  4046  compleq  4093  ssequn1  4127  unss  4131  rexun  4137  ralunb  4138  elin3  4147  inass  4169  ssin  4180  elsymdif  4199  nssinpss  4208  dfun2  4211  difin  4213  indi  4225  indifdi  4235  difin2  4242  eq0  4291  ssdif0  4307  inn0f  4312  inssdif0  4315  ab0w  4320  ab0  4321  ab0orv  4324  abn0  4326  rabeq0w  4328  rabeq0  4329  disj3  4395  ssundif  4428  ralidmw  4457  dfif2  4469  eldifpr  4603  rexdifpr  4604  rexsns  4616  snprc  4662  reusn  4672  difsnpss  4751  tpss  4781  pwpr  4845  eluni2  4855  elunirab  4866  uniun  4874  unissb  4884  elintrab  4903  ssintrab  4914  intun  4923  iuncom  4942  iuncom4  4943  iunab  4995  ssiinf  4998  iunn0  5010  iinab  5011  iunin2  5014  iinun2  5016  iundif2  5017  iunun  5036  iunxun  5037  iunxiun  5040  sspwuni  5043  iinpw  5049  cbvdisj  5063  cbvdisjv  5064  disjor  5068  brun  5137  brin  5138  brdif  5139  dftr2  5195  dftr5  5197  intexrab  5284  inuni  5287  ssext  5401  pweqb  5403  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  7057  fsn  7082  imaiun  7193  isocnv2  7279  isocnv3  7280  isores2  7281  isomin  7285  eqoprab2bw  7430  eqoprab2b  7431  elpwpwel  7714  sucexb  7751  onsucb  7761  dflim4  7792  fiun  7889  f1iun  7890  f11o  7893  opabex3d  7911  opabex3rd  7912  opabex3  7913  dfopab2  7998  dfoprab3s  7999  fmpox  8013  fparlem1  8055  fparlem2  8056  tpostpos  8189  frrlem9  8237  dfsmo2  8280  brwitnlem  8435  oarec  8490  naddasslem1  8623  naddasslem2  8624  qsid  8721  uniinqs  8737  mapval2  8813  mapsncnv  8834  elixp2  8842  ixpin  8864  brsdom  8914  brdom2  8922  xpassen  9002  brsdom2  9032  unfilem1  9208  fiint  9230  dfsup2  9350  supmo  9358  eqinf  9391  infmo  9403  brttrcl2  9626  rankc1  9785  cp  9806  isinfcard  10005  aceq1  10030  aceq2  10032  dfac5lem3  10038  dfac10b  10053  dfac12a  10062  dffin7-2  10311  dfacfin7  10312  fin1a2lem6  10318  iunfo  10452  konigthlem  10482  axgroth6  10742  axgroth3  10745  sstskm  10756  ltexprlem1  10950  gt0srpr  10992  ltpsrpr  11023  map2psrpr  11024  ltresr  11054  fimaxre3  12093  sup3  12104  supaddc  12114  supmul1  12116  elnn0z  12528  elznn0nn  12529  zmin  12885  xrnemnf  13059  xrnepnf  13060  dfrp2  13338  elioomnf  13388  elxrge0  13401  elfzuzb  13463  fzass4  13507  elfz2nn0  13563  elfzo2  13607  elfzo3  13622  lbfzo0  13645  fzo1lb  13659  fzind2  13734  nn0opthlem1  14221  hashgt23el  14377  cotr2g  14929  rexfiuz  15301  fsumcom2  15727  prodmo  15892  fprodcom2  15940  sinltx  16147  divalglem4  16356  divalglem10  16362  4sqlem12  16918  imasleval  17496  xpsfrnel  17517  xpscf  17520  isssc  17778  isffth2  17876  ispos2  18272  issubmgm  18661  ismhm  18744  issubmndb  18764  nsgacs  19128  isgim  19228  oppgcntz  19330  f1omvdco3  19415  pmtrprfvalrn  19454  efgrelexlemb  19716  pgpfac1  20048  pgpfac  20052  issrg  20160  opprsubg  20323  opprunit  20348  isirred2  20392  opprirred  20393  opprnzrb  20489  isdomn2OLD  20680  opprdomnb  20685  isdomn4r  20687  drngprop  20712  opprdrng  20732  issdrg2  20763  isorng  20829  islss  20920  islbs  21063  unocv  21670  iunocv  21671  isbasis2g  22923  tgval2  22931  ntreq0  23052  isclo2  23063  cmpcov2  23365  is1stc2  23417  1stcelcls  23436  llyi  23449  unisngl  23502  txuni2  23540  xkobval  23561  hausdiag  23620  isfbas2  23810  elfg  23846  fbasrn  23859  fmfnfmlem3  23931  isfcls  23984  alexsubALTlem2  24023  istmd  24049  istgp  24052  istrg  24139  istdrg  24141  istdrg2  24153  isms2  24425  metuel2  24540  restmetu  24545  isngp  24571  isngp2  24572  isngp3  24573  elii1  24912  isncvsngp  25126  iscph  25147  isbn  25315  pmltpc  25427  ovolfcl  25443  finiunmbl  25521  iundisj  25525  dyaddisj  25573  vitalilem1  25585  ellimc3  25856  ig1pval3  26153  plyun0  26172  plydivex  26274  aannenlem2  26306  ellogrn  26536  atandm  26853  atandm3  26855  atans2  26908  elno3  27633  conway  27785  eqcuts2  27792  madeval2  27839  ons2ind  28281  tgjustf  28555  colinearalg  28993  axeuclid  29046  nbgrsym  29446  upgrtrls  29783  upgristrl  29784  dfpth2  29812  usgr2pth0  29848  iswwlks  29919  isclwwlk  30069  clwwlkneq0  30114  h2hlm  31066  issh  31294  chcon2i  31550  chcon1i  31551  chcon3i  31552  chnlei  31571  cmcm2i  31679  cmcm3i  31680  3oalem3  31750  pjdifnormii  31769  pjneli  31809  dfadj2  31971  cnvadj  31978  hhcno  31990  hhcnf  31991  eleigvec  32043  eleigvec2  32044  pjimai  32262  isst  32299  ishst  32300  cvnbtwn4  32375  chrelat4i  32459  2reucom  32564  reuxfrdf  32575  difrab2  32582  inpr0  32617  iunin1f  32642  disjnf  32655  cbvdisjf  32656  disjorf  32664  iundisjf  32674  disjexc  32678  xrdifh  32868  iundisjfi  32884  hashxpe  32895  pmtrprfv2  33164  xrnarchi  33260  isunit2  33316  prmidl0  33525  opprnsg  33559  ccfldextdgrr  33832  cmpcref  34010  ordtconnlem1  34084  isrrext  34160  cntnevol  34388  ddemeas  34396  omssubaddlem  34459  omssubadd  34460  eulerpartleme  34523  eulerpartlemv  34524  eulerpartlemt0  34529  eulerpartlemgvv  34536  eulerpartlemn  34541  ballotlem2  34649  ballotlemodife  34658  oddprm2  34815  bnj257  34866  bnj268  34868  bnj290  34869  bnj312  34871  bnj89  34880  bnj887  34924  bnj976  34936  bnj1019  34938  bnj1146  34949  bnj1385  34990  bnj110  35016  bnj121  35028  bnj130  35032  bnj153  35038  bnj543  35051  bnj580  35071  bnj607  35074  bnj849  35083  bnj882  35084  bnj916  35091  bnj985v  35111  bnj985  35112  bnj1033  35127  bnj1083  35136  bnj1090  35137  bnj1128  35148  bnj1174  35161  bnj1228  35169  onvf1odlem1  35301  erdszelem1  35389  cvmliftlem15  35496  snmlval  35529  satfvsuclem2  35558  satfdm  35567  elmpst  35734  mpstrcl  35739  orbi2iALT  35883  untuni  35907  dfso3  35918  xpab  35924  dftr6  35949  coep  35950  coepr  35951  dffr5  35952  dfso2  35953  cnvco1  35957  cnvco2  35958  eldm3  35959  dfdm5  35971  dfrn5  35972  brsset  36085  idsset  36086  dfon3  36088  dfbigcup2  36095  dfom5b  36108  dffun10  36110  dfiota3  36119  fnimage  36125  brdomain  36129  brrange  36130  brimg  36133  brapply  36134  brcup  36135  brcap  36136  lemsuccf  36137  funpartlem  36140  brrestrict  36147  dfrecs2  36148  brub  36152  altopelaltxp  36174  rmoeqi  36385  rmoeqbii  36386  reueqi  36387  reueqbii  36388  sbceqbii  36389  disjeq1i  36390  cbvralvw2  36424  cbvrexvw2  36425  cbvrmovw2  36426  cbvreuvw2  36427  cbvsbcvw2  36428  cbvdisjvw2  36433  trer  36514  filnetlem4  36579  df3nandALT1  36597  imnand2  36600  mh-unprimbi  36742  bj-dfbi5  36855  bj-bixor  36872  bj-dfsbc  36962  bj-nnfnt  37063  bj-csbsnlem  37226  bj-rcleqf  37348  bj-sscon  37352  bj-pw0ALT  37372  bj-restpw  37420  bj-opelidb1  37483  bj-imdiridlem  37515  bj-imdirco  37520  wl-df3xor2  37799  wl-3xorrot  37807  wl-3xorcoma  37808  wl-3xornot  37811  wl-df2-3mintru2  37815  wl-df3-3mintru2  37816  wl-df4-3mintru2  37817  wl-equsalvw  37877  wl-sb9v  37888  iundif1  37929  poimirlem25  37980  poimirlem26  37981  poimirlem30  37985  ismblfin  37996  mbfposadd  38002  itg2addnclem2  38007  ftc1anc  38036  inixp  38063  prdstotbnd  38129  heibor1lem  38144  isrngohom  38300  isidl  38349  isfldidl2  38404  isdmn3  38409  sbccom2lem  38459  triantru3  38571  vvdifopab  38600  brres2  38608  eldmqsres  38628  inxpss  38652  ref5  38654  n0el2  38670  dfsucmap3  38798  trcoss2  38909  dfeqvrel2  39009  dfeqvrel3  39010  redundeq1  39048  redundpbi1  39050  refrelredund4  39054  funALTVfun  39118  dfeldisj3  39146  dfeldisj5  39148  pet0  39253  petid  39255  petidres  39257  petinidres  39259  petxrnidres  39261  mpet  39288  petincnvepres  39298  pet  39300  pmapglbx  40229  lhpexle3  40472  cdleme25cv  40818  dicelval3  41640  diclspsn  41654  lcfls1c  41996  sn-axrep5v  42672  sn-iotalem  42676  psspwb  42683  redvmptabs  42806  eu6w  43123  moxfr  43138  fphpd  43262  uniel  43663  dflim6  43710  onsucf1olem  43716  dflim7  43719  omge2  43744  oenassex  43764  safesnsupfilb  43863  ifpim1  43914  ifpnot  43915  ifpid2  43916  ifpim2  43917  ifpxorcor  43921  ifpnot23  43923  ifpananb  43951  ifpnannanb  43952  ifpxorxorb  43956  rp-fakeinunass  43960  snen1g  43969  pren2  43998  alephiso2  44003  undmrnresiss  44049  cnvssco  44051  cotrintab  44059  cnviun  44095  imaiun1  44096  coiun1  44097  elintima  44098  frege133d  44210  frege54cor0a  44308  or3or  44468  andi3or  44469  ntrneik4w  44545  k0004lem1  44592  ismnuprim  44739  ismnushort  44746  undisjrab  44751  nzss  44762  pm10.541  44812  compab  44886  onfrALTlem5  44987  onfrALTlem5VD  45329  rext0  45383  wfaxun  45444  brpermmodel  45448  permaxrep  45451  permaxpow  45454  permac8prim  45459  eluni2f  45551  euabsneu  47488  aiotaexb  47549  aiotavb  47550  r19.32  47558  3an4ancom24  47729  ichn  47928  ichcom  47931  ichbi12i  47932  prproropf1olem0  47974  pairreueq  47982  clnbgrsym  48326  usgrexmpl2nb0  48519  usgrexmpl2nb1  48520  usgrexmpl2nb2  48521  usgrexmpl2nb3  48522  usgrexmpl2nb4  48523  usgrexmpl2nb5  48524  sgrp2sgrp  48716  islindeps  48941  elbigo  49039  reutruALT  49292  coxp  49320  tposres0  49364  catcinv  49886  isthincd2  49924  setrec1lem3  50176  elpg  50201