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  806  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  1155  3orbi123i  1156  3jaob  1428  an6  1447  3or6  1449  an3andi  1484  an33rean  1485  nancom  1496  xorass  1515  anxordi  1526  norass  1537  hadbi  1598  hadcoma  1599  hadcomb  1600  hadnot  1602  cador  1608  cadan  1609  cadcoma  1612  cadnot  1615  nic-axALT  1674  19.26-3an  1872  19.43OLD  1883  19.32v  1940  19.31v  1941  19.42v  1953  4exdistr  1961  cbvexvw  2037  exexw  2052  sb3an  2082  sbcom4  2090  sbbiiev  2093  excom  2163  sbal  2170  19.32  2234  19.31  2235  19.42  2237  equsalv  2268  sbex  2281  sbrim  2304  sbor  2306  sbbi  2307  sbnfOLD  2312  cbvex2v  2342  eeeanv  2348  sbnf2  2356  cbvsbvf  2361  cbvex2  2410  equsal  2415  dfsb3  2492  mo4  2559  eu6  2567  eubii  2578  dfeu  2588  sb8eulem  2591  sb8mo  2594  cbvmovw  2595  cbvmow  2596  cbveuvw  2598  cbveuw  2599  cbveuALT  2601  eu1  2603  sbmo  2607  cbvabv  2799  cbvabw  2800  cbvab  2801  eqabcb  2869  nfceqi  2888  ralbii2  3071  rexbii2  3072  r19.26-3  3092  r19.43  3101  r2allem  3121  r19.21vOLD  3159  r19.42v  3169  r19.32v  3170  reeanlem  3208  3reeanv  3210  cbvralvw  3215  cbvrexvw  3216  ralcom  3265  ralcomf  3276  rexcomf  3277  cbvralfw  3278  cbvralsvw  3290  cbvralf  3334  cbvrexf  3335  reu5  3356  rmobiia  3360  reubiia  3361  rmoanidOLD  3366  reuanidOLD  3367  rmo5  3374  cbvrmovw  3377  cbvreuvw  3378  cbvrmow  3381  cbvreuw  3382  cbvreu  3397  cbvrmo  3398  rabid2f  3437  abv  3459  abvALT  3460  ceqsal  3485  ceqsalv  3487  cgsex4gOLD  3495  ceqsex3v  3503  ceqsex4v  3504  ceqsex8v  3506  reurab  3672  eueq  3679  reu2  3696  reu6  3697  reu3  3698  rmo4  3701  rmo3f  3705  2reu5  3729  cbvsbcw  3786  cbvsbcvw  3787  cbvsbc  3788  sbc3an  3818  sbccomlemOLD  3833  rmo3  3852  rmoanim  3857  rmoanimALT  3858  cbvralcsf  3904  cbvrexcsf  3905  cbvreucsf  3906  eqss  3962  uniiunlem  4050  sspsstri  4068  compleq  4115  ssequn1  4149  unss  4153  rexun  4159  ralunb  4160  elin3  4169  inass  4191  ssin  4202  elsymdif  4221  nssinpss  4230  dfun2  4233  difin  4235  indi  4247  indifdi  4257  difin2  4264  ssdif0  4329  inn0f  4334  inssdif0  4337  ab0  4343  abn0  4348  rabeq0w  4350  rabeq0  4351  disj  4413  disj3  4417  ssundif  4451  ralidmw  4471  dfif2  4490  eldifpr  4622  rexdifpr  4623  rexsns  4635  snprc  4681  reusn  4691  difsnpss  4771  tpss  4801  pwpr  4865  eluni2  4875  elunirab  4886  uniun  4894  unissb  4903  unissbOLD  4904  elintrab  4924  ssintrab  4935  intun  4944  iuncom  4963  iuncom4  4964  iunab  5015  ssiinf  5018  iunn0  5031  iinab  5032  iunin2  5035  iinun2  5037  iundif2  5038  iunun  5057  iunxun  5058  iunxiun  5061  sspwuni  5064  iinpw  5070  cbvdisj  5084  cbvdisjv  5085  disjor  5089  brun  5158  brin  5159  brdif  5160  dftr2  5216  dftr5  5218  intexrab  5302  inuni  5305  ssext  5414  pweqb  5416  otth2  5443  otthne  5446  propeqop  5467  vopelopabsb  5489  eqopab2bw  5508  eqopab2b  5512  pwin  5529  pwun  5531  dffr6  5594  elxp2  5662  otelxp  5682  xpiundi  5709  xpiundir  5710  poinxp  5719  soinxp  5720  frinxp  5721  seinxp  5722  weinxp  5723  inopab  5792  difopab  5793  difopabOLD  5794  inxp  5795  raliunxp  5803  rexiunxp  5804  rexxpf  5811  iunxpf  5812  cnvco  5849  dmiun  5877  dmuni  5878  dm0rn0  5888  dmres  5983  restidsing  6024  cnvsymOLDOLD  6087  asymref  6089  codir  6093  qfto  6094  cnvopab  6110  cnvopabOLD  6111  cnvdif  6116  rniun  6120  dminss  6126  imainss  6127  difxp  6137  xpdifid  6141  dmsnn0  6180  cnvcnvsn  6192  cnvresima  6203  resco  6223  imaco  6224  rnco  6225  coiun  6229  coass  6238  ressn  6258  cnviin  6259  cnvpo  6260  cnvso  6261  xpco  6262  opreu2reurex  6267  dfpo2  6269  imaindm  6272  dflim2  6390  funcnv  6585  funcnv3  6586  fncnv  6589  fun11  6590  imadif  6600  fnres  6645  dfmpt3  6652  mptfnf  6653  fnopabg  6655  fint  6739  fin  6740  fores  6782  dff1o3  6806  f1ompt  7083  fsn  7107  imaiun  7219  isocnv2  7306  isocnv3  7307  isores2  7308  isomin  7312  eqoprab2bw  7459  eqoprab2b  7460  elpwpwel  7743  sucexb  7780  onsucb  7792  dflim4  7824  fiun  7921  f1iun  7922  f11o  7925  opabex3d  7944  opabex3rd  7945  opabex3  7946  dfopab2  8031  dfoprab3s  8032  fmpox  8046  fparlem1  8091  fparlem2  8092  tpostpos  8225  frrlem9  8273  dfsmo2  8316  brwitnlem  8471  oarec  8526  naddasslem1  8658  naddasslem2  8659  qsid  8754  uniinqs  8770  mapval2  8845  mapsncnv  8866  elixp2  8874  ixpin  8896  brsdom  8946  brdom2  8953  xpassen  9035  brsdom2  9065  dif1enOLD  9126  unfilem1  9254  fiint  9277  fiintOLD  9278  dfsup2  9395  supmo  9403  eqinf  9436  infmo  9448  brttrcl2  9667  rankc1  9823  cp  9844  isinfcard  10045  aceq1  10070  aceq2  10072  dfac5lem3  10078  dfac10b  10093  dfac12a  10102  dffin7-2  10351  dfacfin7  10352  fin1a2lem6  10358  iunfo  10492  konigthlem  10521  axgroth6  10781  axgroth3  10784  sstskm  10795  ltexprlem1  10989  gt0srpr  11031  ltpsrpr  11062  map2psrpr  11063  ltresr  11093  fimaxre3  12129  sup3  12140  supaddc  12150  supmul1  12152  elnn0z  12542  elznn0nn  12543  zmin  12903  xrnemnf  13077  xrnepnf  13078  dfrp2  13355  elioomnf  13405  elxrge0  13418  elfzuzb  13479  fzass4  13523  elfz2nn0  13579  elfzo2  13623  elfzo3  13637  lbfzo0  13660  fzo1lb  13674  fzind2  13746  nn0opthlem1  14233  hashgt23el  14389  cotr2g  14942  rexfiuz  15314  fsumcom2  15740  prodmo  15902  fprodcom2  15950  sinltx  16157  divalglem4  16366  divalglem10  16372  4sqlem12  16927  imasleval  17504  xpsfrnel  17525  xpscf  17528  isssc  17782  isffth2  17880  ispos2  18276  issubmgm  18629  ismhm  18712  issubmndb  18732  nsgacs  19094  isgim  19194  oppgcntz  19296  f1omvdco3  19379  pmtrprfvalrn  19418  efgrelexlemb  19680  pgpfac1  20012  pgpfac  20016  issrg  20097  opprsubg  20261  opprunit  20286  isirred2  20330  opprirred  20331  opprnzrb  20430  isdomn2OLD  20621  opprdomnb  20626  isdomn4r  20628  drngprop  20653  opprdrng  20673  issdrg2  20704  islss  20840  islbs  20983  unocv  21589  iunocv  21590  isbasis2g  22835  tgval2  22843  ntreq0  22964  isclo2  22975  cmpcov2  23277  is1stc2  23329  1stcelcls  23348  llyi  23361  unisngl  23414  txuni2  23452  xkobval  23473  hausdiag  23532  isfbas2  23722  elfg  23758  fbasrn  23771  fmfnfmlem3  23843  isfcls  23896  alexsubALTlem2  23935  istmd  23961  istgp  23964  istrg  24051  istdrg  24053  istdrg2  24065  isms2  24338  metuel2  24453  restmetu  24458  isngp  24484  isngp2  24485  isngp3  24486  elii1  24831  isncvsngp  25049  iscph  25070  isbn  25238  pmltpc  25351  ovolfcl  25367  finiunmbl  25445  iundisj  25449  dyaddisj  25497  vitalilem1  25509  ellimc3  25780  ig1pval3  26083  plyun0  26102  plydivex  26205  aannenlem2  26237  ellogrn  26468  atandm  26786  atandm3  26788  atans2  26841  elno3  27567  conway  27711  eqscut2  27718  madeval2  27761  tgjustf  28400  colinearalg  28837  axeuclid  28890  nbgrsym  29290  upgrtrls  29629  upgristrl  29630  dfpth2  29659  usgr2pth0  29695  iswwlks  29766  isclwwlk  29913  clwwlkneq0  29958  h2hlm  30909  issh  31137  chcon2i  31393  chcon1i  31394  chcon3i  31395  chnlei  31414  cmcm2i  31522  cmcm3i  31523  3oalem3  31593  pjdifnormii  31612  pjneli  31652  dfadj2  31814  cnvadj  31821  hhcno  31833  hhcnf  31834  eleigvec  31886  eleigvec2  31887  pjimai  32105  isst  32142  ishst  32143  cvnbtwn4  32218  chrelat4i  32302  2reucom  32409  reuxfrdf  32420  difrab2  32427  inpr0  32461  iunin1f  32486  disjnf  32499  cbvdisjf  32500  disjorf  32508  iundisjf  32518  disjexc  32522  xrdifh  32703  iundisjfi  32719  hashxpe  32732  pmtrprfv2  33045  xrnarchi  33138  isunit2  33191  isorng  33277  prmidl0  33421  opprnsg  33455  ccfldextdgrr  33667  cmpcref  33840  ordtconnlem1  33914  isrrext  33990  cntnevol  34218  ddemeas  34226  omssubaddlem  34290  omssubadd  34291  eulerpartleme  34354  eulerpartlemv  34355  eulerpartlemt0  34360  eulerpartlemgvv  34367  eulerpartlemn  34372  ballotlem2  34480  ballotlemodife  34489  oddprm2  34646  bnj257  34697  bnj268  34699  bnj290  34700  bnj312  34702  bnj89  34711  bnj887  34755  bnj976  34767  bnj1019  34769  bnj1146  34781  bnj1385  34822  bnj110  34848  bnj121  34860  bnj130  34864  bnj153  34870  bnj543  34883  bnj580  34903  bnj607  34906  bnj849  34915  bnj882  34916  bnj916  34923  bnj985v  34943  bnj985  34944  bnj1033  34959  bnj1083  34968  bnj1090  34969  bnj1128  34980  bnj1174  34993  bnj1228  35001  onvf1odlem1  35090  erdszelem1  35178  cvmliftlem15  35285  snmlval  35318  satfvsuclem2  35347  satfdm  35356  elmpst  35523  mpstrcl  35528  orbi2iALT  35672  untuni  35696  dfso3  35707  xpab  35713  dftr6  35738  coep  35739  coepr  35740  dffr5  35741  dfso2  35742  cnvco1  35746  cnvco2  35747  eldm3  35748  dfdm5  35760  dfrn5  35761  brsset  35877  idsset  35878  dfon3  35880  dfbigcup2  35887  dfom5b  35900  dffun10  35902  dfiota3  35911  fnimage  35917  brdomain  35921  brrange  35922  brimg  35925  brapply  35926  brcup  35927  brcap  35928  brsuccf  35929  funpartlem  35930  brrestrict  35937  dfrecs2  35938  brub  35942  altopelaltxp  35964  rmoeqi  36175  rmoeqbii  36176  reueqi  36177  reueqbii  36178  sbceqbii  36179  disjeq1i  36180  cbvralvw2  36214  cbvrexvw2  36215  cbvrmovw2  36216  cbvreuvw2  36217  cbvsbcvw2  36218  cbvdisjvw2  36223  trer  36304  filnetlem4  36369  df3nandALT1  36387  imnand2  36390  bj-dfbi5  36562  bj-bixor  36579  bj-nnfnt  36728  bj-csbsnlem  36891  bj-rcleqf  37013  bj-sscon  37017  bj-pw0ALT  37037  bj-restpw  37080  bj-opelidb1  37141  bj-imdiridlem  37173  bj-imdirco  37178  wl-df3xor2  37457  wl-3xorrot  37465  wl-3xorcoma  37466  wl-3xornot  37469  wl-df2-3mintru2  37473  wl-df3-3mintru2  37474  wl-df4-3mintru2  37475  wl-equsalvw  37526  wl-sb9v  37537  iundif1  37588  poimirlem25  37639  poimirlem26  37640  poimirlem30  37644  ismblfin  37655  mbfposadd  37661  itg2addnclem2  37666  ftc1anc  37695  inixp  37722  prdstotbnd  37788  heibor1lem  37803  isrngohom  37959  isidl  38008  isfldidl2  38063  isdmn3  38068  sbccom2lem  38118  triantru3  38218  vvdifopab  38249  brres2  38257  eldmqsres  38275  inxpss  38299  ref5  38301  n0el2  38317  trcoss2  38475  dfeqvrel2  38581  dfeqvrel3  38582  redundeq1  38620  redundpbi1  38622  refrelredund4  38626  funALTVfun  38690  dfeldisj3  38711  dfeldisj5  38713  pet0  38807  petid  38809  petidres  38811  petinidres  38813  petxrnidres  38815  mpet  38831  petincnvepres  38841  pet  38843  pmapglbx  39763  lhpexle3  40006  cdleme25cv  40352  dicelval3  41174  diclspsn  41188  lcfls1c  41530  sn-axrep5v  42204  sn-iotalem  42209  psspwb  42216  redvmptabs  42348  eu6w  42664  moxfr  42680  fphpd  42804  uniel  43206  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  44283  ismnushort  44290  undisjrab  44295  nzss  44306  pm10.541  44356  compab  44431  onfrALTlem5  44532  onfrALTlem5VD  44874  rext0  44928  wfaxun  44989  brpermmodel  44993  permaxrep  44996  permaxpow  44999  permac8prim  45004  eluni2f  45097  euabsneu  47029  aiotaexb  47090  aiotavb  47091  r19.32  47099  3an4ancom24  47270  ichn  47457  ichcom  47460  ichbi12i  47461  prproropf1olem0  47503  pairreueq  47511  clnbgrsym  47838  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2nb4  48026  usgrexmpl2nb5  48027  sgrp2sgrp  48216  islindeps  48442  elbigo  48540  reutruALT  48793  coxp  48821  tposres0  48865  catcinv  49388  isthincd2  49426  setrec1lem3  49678  elpg  49703