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  647  pm4.14  806  or4  925  orimdi  929  orbidi  953  ordi  1006  ordir  1007  andir  1009  dfbi3  1050  dfifp7  1070  ifpdfbi  1071  ifpn  1074  3orrot  1092  3orcoma  1093  3ioran  1106  3ianor  1107  3anbi123i  1155  3orbi123i  1156  3jaob  1426  an6  1445  3or6  1447  an3andi  1482  an33rean  1483  nancom  1493  xorass  1512  anxordi  1523  norass  1534  hadbi  1595  hadcoma  1596  hadcomb  1597  hadnot  1599  cador  1605  cadan  1606  cadcoma  1609  cadnot  1612  nic-axALT  1672  nfnbiOLD  1854  19.26-3an  1871  19.43OLD  1882  19.32v  1939  19.31v  1940  19.42v  1953  4exdistr  1961  cbvexvw  2036  exexw  2051  sb3an  2081  sbcom4  2089  sbbiiev  2092  excom  2163  sbal  2170  19.32  2234  19.31  2235  19.42  2237  equsalv  2268  sbex  2285  sbrim  2308  sbor  2311  sbbi  2312  sbnfOLD  2317  cbvex2v  2350  eeeanv  2356  sbnf2  2364  cbvsbvf  2369  cbvex2  2420  equsal  2425  dfsb3  2502  mo4  2569  eu6  2577  eubii  2588  dfeu  2598  sb8eulem  2601  sb8mo  2604  cbvmovw  2605  cbvmow  2606  cbveuvw  2608  cbveuw  2609  cbveuALT  2611  eu1  2613  sbmo  2617  cbvabv  2815  cbvabw  2816  cbvab  2817  eqabcb  2886  nfceqi  2905  sbabelOLD  2945  ralbii2  3095  rexbii2  3096  r19.26-3  3118  r19.43  3128  r2allem  3148  r19.21vOLD  3187  r19.42v  3197  r19.32v  3198  reeanlem  3234  3reeanv  3236  2ralorOLD  3238  cbvralvw  3243  cbvrexvw  3244  ralcom4OLD  3293  ralcom  3295  ralcomf  3308  rexcomf  3309  cbvralfw  3310  cbvralsvw  3323  cbvralf  3368  cbvrexf  3369  reu5  3390  rmobiia  3394  reubiia  3395  rmoanidOLD  3400  reuanidOLD  3401  rmo5  3408  cbvrmovw  3411  cbvreuvw  3412  moelOLD  3413  cbvrmow  3417  cbvreuw  3418  cbvreuwOLD  3423  cbvreu  3435  cbvrmo  3436  rabid2f  3476  rabid2OLD  3479  abv  3500  abvALT  3501  ceqsal  3527  ceqsalv  3529  cgsex4gOLD  3539  ceqsex3v  3549  ceqsex4v  3550  ceqsex8v  3552  reurab  3723  eueq  3730  reu2  3747  reu6  3748  reu3  3749  rmo4  3752  rmo3f  3756  2reu5  3780  cbvsbcw  3838  cbvsbcvw  3839  cbvsbc  3840  sbc3an  3874  sbccomlemOLD  3892  rmo3  3911  rmoanim  3916  rmoanimALT  3917  cbvralcsf  3966  cbvrexcsf  3967  cbvreucsf  3968  eqss  4024  uniiunlem  4110  sspsstri  4128  compleq  4175  ssequn1  4209  unss  4213  rexun  4219  ralunb  4220  elin3  4229  inass  4249  ssin  4260  elsymdif  4277  nssinpss  4286  dfun2  4289  difin  4291  indi  4303  indifdi  4313  difin2  4320  ssdif0  4389  inn0f  4394  inssdif0  4397  ab0  4402  abn0  4408  rabeq0w  4410  rabeq0  4411  disj  4473  disj3  4477  ssundif  4511  ralidmw  4531  dfif2  4550  eldifpr  4680  rexdifpr  4681  rexsns  4693  snprc  4742  reusn  4752  difsnpss  4832  tpss  4862  pwpr  4925  eluni2  4935  elunirab  4946  uniun  4954  unissb  4963  unissbOLD  4964  elintrab  4984  ssintrab  4995  intun  5004  iuncom  5022  iuncom4  5023  iunab  5074  ssiinf  5077  iunn0  5090  iinab  5091  iunin2  5094  iinun2  5096  iundif2  5097  iunun  5116  iunxun  5117  iunxiun  5120  sspwuni  5123  iinpw  5129  cbvdisj  5143  cbvdisjv  5144  disjor  5148  brun  5217  brin  5218  brdif  5219  dftr2  5285  dftr5  5287  intexrab  5365  inuni  5368  ssext  5474  pweqb  5476  otth2  5503  otthne  5506  propeqop  5526  vopelopabsb  5548  eqopab2bw  5567  eqopab2b  5571  pwin  5589  pwun  5591  dffr6  5655  elxp2  5724  otelxp  5744  xpiundi  5770  xpiundir  5771  poinxp  5780  soinxp  5781  frinxp  5782  seinxp  5783  weinxp  5784  inopab  5853  difopab  5854  difopabOLD  5855  inxp  5856  raliunxp  5864  rexiunxp  5865  rexxpf  5872  iunxpf  5873  cnvco  5910  dmiun  5938  dmuni  5939  dm0rn0  5949  dmres  6041  restidsing  6082  cnvsymOLDOLD  6146  asymref  6148  codir  6152  qfto  6153  cnvopab  6169  cnvopabOLD  6170  cnvdif  6175  rniun  6179  dminss  6184  imainss  6185  difxp  6195  xpdifid  6199  dmsnn0  6238  cnvcnvsn  6250  cnvresima  6261  resco  6281  imaco  6282  rnco  6283  coiun  6287  coass  6296  ressn  6316  cnviin  6317  cnvpo  6318  cnvso  6319  xpco  6320  opreu2reurex  6325  dfpo2  6327  imaindm  6330  dflim2  6452  funcnv  6647  funcnv3  6648  fncnv  6651  fun11  6652  imadif  6662  fnres  6707  dfmpt3  6714  mptfnf  6715  fnopabg  6717  fint  6800  fin  6801  fores  6844  dff1o3  6868  f1ompt  7145  fsn  7169  imaiun  7282  isocnv2  7367  isocnv3  7368  isores2  7369  isomin  7373  eqoprab2bw  7520  eqoprab2b  7521  elpwpwel  7802  sucexb  7840  onsucb  7853  dflim4  7885  fiun  7983  f1iun  7984  f11o  7987  opabex3d  8006  opabex3rd  8007  opabex3  8008  dfopab2  8093  dfoprab3s  8094  fmpox  8108  fparlem1  8153  fparlem2  8154  tpostpos  8287  frrlem9  8335  wfrlem8OLD  8372  wfrfunOLD  8375  dfsmo2  8403  brwitnlem  8563  oarec  8618  naddasslem1  8750  naddasslem2  8751  qsid  8841  uniinqs  8855  mapval2  8930  mapsncnv  8951  elixp2  8959  ixpin  8981  brsdom  9035  brdom2  9042  xpassen  9132  brsdom2  9163  dif1enOLD  9228  unfilem1  9371  fiint  9394  fiintOLD  9395  dfsup2  9513  supmo  9521  eqinf  9553  infmo  9564  brttrcl2  9783  rankc1  9939  cp  9960  isinfcard  10161  aceq1  10186  aceq2  10188  dfac5lem3  10194  dfac10b  10209  dfac12a  10218  dffin7-2  10467  dfacfin7  10468  fin1a2lem6  10474  iunfo  10608  konigthlem  10637  axgroth6  10897  axgroth3  10900  sstskm  10911  ltexprlem1  11105  gt0srpr  11147  ltpsrpr  11178  map2psrpr  11179  ltresr  11209  fimaxre3  12241  sup3  12252  supaddc  12262  supmul1  12264  elnn0z  12652  elznn0nn  12653  zmin  13009  xrnemnf  13180  xrnepnf  13181  dfrp2  13456  elioomnf  13504  elxrge0  13517  elfzuzb  13578  fzass4  13622  elfz2nn0  13675  elfzo2  13719  elfzo3  13733  lbfzo0  13756  fzind2  13835  nn0opthlem1  14317  hashgt23el  14473  cotr2g  15025  rexfiuz  15396  fsumcom2  15822  prodmo  15984  fprodcom2  16032  sinltx  16237  divalglem4  16444  divalglem10  16450  4sqlem12  17003  imasleval  17601  xpsfrnel  17622  xpscf  17625  isssc  17881  isffth2  17983  ispos2  18385  issubmgm  18740  ismhm  18820  issubmndb  18840  nsgacs  19202  isgim  19302  oppgcntz  19407  f1omvdco3  19491  pmtrprfvalrn  19530  efgrelexlemb  19792  pgpfac1  20124  pgpfac  20128  issrg  20215  opprsubg  20378  opprunit  20403  isirred2  20447  opprirred  20448  opprnzrb  20547  isdomn2OLD  20734  opprdomnb  20739  isdomn4r  20741  drngprop  20766  opprdrng  20786  issdrg2  20818  islss  20955  islbs  21098  unocv  21721  iunocv  21722  isbasis2g  22976  tgval2  22984  ntreq0  23106  isclo2  23117  cmpcov2  23419  is1stc2  23471  1stcelcls  23490  llyi  23503  unisngl  23556  txuni2  23594  xkobval  23615  hausdiag  23674  isfbas2  23864  elfg  23900  fbasrn  23913  fmfnfmlem3  23985  isfcls  24038  alexsubALTlem2  24077  istmd  24103  istgp  24106  istrg  24193  istdrg  24195  istdrg2  24207  isms2  24481  metuel2  24599  restmetu  24604  isngp  24630  isngp2  24631  isngp3  24632  elii1  24983  isncvsngp  25202  iscph  25223  isbn  25391  pmltpc  25504  ovolfcl  25520  finiunmbl  25598  iundisj  25602  dyaddisj  25650  vitalilem1  25662  ellimc3  25934  ig1pval3  26237  plyun0  26256  plydivex  26357  aannenlem2  26389  ellogrn  26619  atandm  26937  atandm3  26939  atans2  26992  elno3  27718  conway  27862  eqscut2  27869  madeval2  27910  tgjustf  28499  colinearalg  28943  axeuclid  28996  nbgrsym  29398  upgrtrls  29737  upgristrl  29738  usgr2pth0  29801  iswwlks  29869  isclwwlk  30016  clwwlkneq0  30061  h2hlm  31012  issh  31240  chcon2i  31496  chcon1i  31497  chcon3i  31498  chnlei  31517  cmcm2i  31625  cmcm3i  31626  3oalem3  31696  pjdifnormii  31715  pjneli  31755  dfadj2  31917  cnvadj  31924  hhcno  31936  hhcnf  31937  eleigvec  31989  eleigvec2  31990  pjimai  32208  isst  32245  ishst  32246  cvnbtwn4  32321  chrelat4i  32405  2reucom  32508  reuxfrdf  32519  difrab2  32526  inpr0  32560  iunin1f  32580  disjnf  32592  cbvdisjf  32593  disjorf  32601  iundisjf  32611  disjexc  32615  xrdifh  32785  iundisjfi  32801  hashxpe  32814  pmtrprfv2  33081  xrnarchi  33164  isunit2  33220  isorng  33294  prmidl0  33443  opprnsg  33477  ccfldextdgrr  33682  cmpcref  33796  ordtconnlem1  33870  isrrext  33946  cntnevol  34192  ddemeas  34200  omssubaddlem  34264  omssubadd  34265  eulerpartleme  34328  eulerpartlemv  34329  eulerpartlemt0  34334  eulerpartlemgvv  34341  eulerpartlemn  34346  ballotlem2  34453  ballotlemodife  34462  oddprm2  34632  bnj257  34683  bnj268  34685  bnj290  34686  bnj312  34688  bnj89  34697  bnj887  34741  bnj976  34753  bnj1019  34755  bnj1146  34767  bnj1385  34808  bnj110  34834  bnj121  34846  bnj130  34850  bnj153  34856  bnj543  34869  bnj580  34889  bnj607  34892  bnj849  34901  bnj882  34902  bnj916  34909  bnj985v  34929  bnj985  34930  bnj1033  34945  bnj1083  34954  bnj1090  34955  bnj1128  34966  bnj1174  34979  bnj1228  34987  erdszelem1  35159  cvmliftlem15  35266  snmlval  35299  satfvsuclem2  35328  satfdm  35337  elmpst  35504  mpstrcl  35509  orbi2iALT  35653  untuni  35671  dfso3  35682  xpab  35688  dftr6  35713  coep  35714  coepr  35715  dffr5  35716  dfso2  35717  cnvco1  35721  cnvco2  35722  eldm3  35723  dfdm5  35736  dfrn5  35737  brsset  35853  idsset  35854  dfon3  35856  dfbigcup2  35863  dfom5b  35876  dffun10  35878  dfiota3  35887  fnimage  35893  brdomain  35897  brrange  35898  brimg  35901  brapply  35902  brcup  35903  brcap  35904  brsuccf  35905  funpartlem  35906  brrestrict  35913  dfrecs2  35914  brub  35918  altopelaltxp  35940  rmoeqi  36151  rmoeqbii  36152  reueqi  36153  reueqbii  36154  sbceqbii  36155  disjeq1i  36156  cbvralvw2  36192  cbvrexvw2  36193  cbvrmovw2  36194  cbvreuvw2  36195  cbvsbcvw2  36196  cbvdisjvw2  36201  trer  36282  filnetlem4  36347  df3nandALT1  36365  imnand2  36368  bj-dfbi5  36540  bj-bixor  36557  bj-nnfnt  36706  bj-csbsnlem  36869  bj-rcleqf  36991  bj-sscon  36995  bj-pw0ALT  37015  bj-restpw  37058  bj-opelidb1  37119  bj-imdiridlem  37151  bj-imdirco  37156  wl-df3xor2  37435  wl-3xorrot  37443  wl-3xorcoma  37444  wl-3xornot  37447  wl-df2-3mintru2  37451  wl-df3-3mintru2  37452  wl-df4-3mintru2  37453  wl-equsalvw  37492  wl-sb9v  37503  iundif1  37554  poimirlem25  37605  poimirlem26  37606  poimirlem30  37610  ismblfin  37621  mbfposadd  37627  itg2addnclem2  37632  ftc1anc  37661  inixp  37688  prdstotbnd  37754  heibor1lem  37769  isrngohom  37925  isidl  37974  isfldidl2  38029  isdmn3  38034  sbccom2lem  38084  triantru3  38184  vvdifopab  38216  brres2  38224  eldmqsres  38243  inxpss  38267  ref5  38269  n0el2  38289  trcoss2  38440  dfeqvrel2  38546  dfeqvrel3  38547  redundeq1  38585  redundpbi1  38587  refrelredund4  38591  funALTVfun  38654  dfeldisj3  38675  dfeldisj5  38677  pet0  38771  petid  38773  petidres  38775  petinidres  38777  petxrnidres  38779  mpet  38795  petincnvepres  38805  pet  38807  pmapglbx  39726  lhpexle3  39969  cdleme25cv  40315  dicelval3  41137  diclspsn  41151  lcfls1c  41493  sn-axrep5v  42209  sn-iotalem  42214  psspwb  42221  eu6w  42631  moxfr  42648  fphpd  42772  uniel  43178  dflim6  43226  onsucf1olem  43232  dflim7  43235  omge2  43260  oenassex  43280  safesnsupfilb  43380  ifpim1  43431  ifpnot  43432  ifpid2  43433  ifpim2  43434  ifpxorcor  43438  ifpnot23  43440  ifpananb  43468  ifpnannanb  43469  ifpxorxorb  43473  rp-fakeinunass  43477  snen1g  43486  pren2  43515  alephiso2  43520  undmrnresiss  43566  cnvssco  43568  cotrintab  43576  cnviun  43612  imaiun1  43613  coiun1  43614  elintima  43615  frege133d  43727  frege54cor0a  43825  or3or  43985  andi3or  43986  ntrneik4w  44062  k0004lem1  44109  ismnuprim  44263  ismnushort  44270  undisjrab  44275  nzss  44286  pm10.541  44336  compab  44411  onfrALTlem5  44513  onfrALTlem5VD  44856  eluni2f  45005  euabsneu  46943  aiotaexb  47004  aiotavb  47005  r19.32  47013  3an4ancom24  47184  ichn  47330  ichcom  47333  ichbi12i  47334  prproropf1olem0  47376  pairreueq  47384  clnbgrsym  47710  usgrexmpl2nb0  47846  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  sgrp2sgrp  47951  islindeps  48182  elbigo  48285  reutruALT  48538  isthincd2  48705  setrec1lem3  48781  elpg  48806