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  1497  xorass  1516  anxordi  1527  norass  1538  hadbi  1599  hadcoma  1600  hadcomb  1601  hadnot  1603  cador  1609  cadan  1610  cadcoma  1613  cadnot  1616  nic-axALT  1675  19.26-3an  1873  19.43OLD  1884  19.32v  1941  19.31v  1942  19.42v  1954  4exdistr  1962  cbvexvw  2038  exexw  2054  sb3an  2084  sbcom4  2092  sbbiiev  2095  excom  2165  sbal  2172  19.32  2236  19.31  2237  19.42  2239  equsalv  2270  sbex  2283  sbrim  2306  sbor  2308  sbbi  2309  sbnfOLD  2314  cbvex2v  2344  eeeanv  2350  sbnf2  2358  cbvsbvf  2363  cbvex2  2412  equsal  2417  dfsb3  2494  mo4  2561  eu6  2569  eubii  2580  dfeu  2590  sb8eulem  2593  sb8mo  2596  cbvmovw  2597  cbvmow  2598  cbveuvw  2600  cbveuw  2601  cbveuALT  2603  eu1  2605  sbmo  2609  cbvabv  2801  cbvabw  2802  cbvab  2803  eqabcbw  2805  eqabcb  2872  nfceqi  2891  ralbii2  3074  rexbii2  3075  r19.26-3  3093  r19.43  3100  r2allem  3120  r19.42v  3164  r19.32v  3165  reeanlem  3203  3reeanv  3205  cbvralvw  3210  cbvrexvw  3211  ralcom  3260  ralcomf  3270  rexcomf  3271  cbvralfw  3272  cbvralsvw  3283  cbvralf  3326  cbvrexf  3327  reu5  3348  rmobiia  3352  reubiia  3353  rmo5  3364  cbvrmovw  3367  cbvreuvw  3368  cbvrmow  3371  cbvreuw  3372  cbvreu  3387  cbvrmo  3388  rabid2f  3426  abv  3448  abvALT  3449  ceqsal  3474  ceqsalv  3476  cgsex4gOLD  3484  ceqsex3v  3491  ceqsex4v  3492  ceqsex8v  3494  reurab  3655  eueq  3662  reu2  3679  reu6  3680  reu3  3681  rmo4  3684  rmo3f  3688  2reu5  3712  cbvsbcw  3769  cbvsbcvw  3770  cbvsbc  3771  sbc3an  3801  sbccomlemOLD  3816  rmo3  3835  rmoanim  3840  rmoanimALT  3841  cbvralcsf  3887  cbvrexcsf  3888  cbvreucsf  3889  eqss  3945  uniiunlem  4032  sspsstri  4050  compleq  4097  ssequn1  4131  unss  4135  rexun  4141  ralunb  4142  elin3  4151  inass  4173  ssin  4184  elsymdif  4203  nssinpss  4212  dfun2  4215  difin  4217  indi  4229  indifdi  4239  difin2  4246  ssdif0  4311  inn0f  4316  inssdif0  4319  ab0  4325  abn0  4330  rabeq0w  4332  rabeq0  4333  disj3  4399  ssundif  4433  ralidmw  4453  dfif2  4472  eldifpr  4606  rexdifpr  4607  rexsns  4619  snprc  4665  reusn  4675  difsnpss  4754  tpss  4784  pwpr  4848  eluni2  4858  elunirab  4869  uniun  4877  unissb  4886  elintrab  4905  ssintrab  4916  intun  4925  iuncom  4944  iuncom4  4945  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  5280  inuni  5283  ssext  5390  pweqb  5392  otth2  5418  otthne  5421  propeqop  5442  vopelopabsb  5464  eqopab2bw  5483  eqopab2b  5487  pwin  5502  pwun  5504  dffr6  5567  elxp2  5635  otelxp  5655  xpiundi  5682  xpiundir  5683  poinxp  5692  soinxp  5693  frinxp  5694  seinxp  5695  weinxp  5696  inopab  5764  difopab  5765  inxp  5766  raliunxp  5774  rexiunxp  5775  rexxpf  5782  iunxpf  5783  cnvco  5820  dmiun  5848  dmuni  5849  dm0rn0  5859  dm0rn0OLD  5860  dmres  5956  restidsing  5997  asymref  6058  codir  6062  qfto  6063  cnvopab  6079  cnvopabOLD  6080  cnvdif  6085  rniun  6089  dminss  6095  imainss  6096  difxp  6106  xpdifid  6110  dmsnn0  6149  cnvcnvsn  6161  cnvresima  6172  resco  6192  imaco  6193  rnco  6194  rncoOLD  6195  coiun  6199  coass  6208  ressn  6227  cnviin  6228  cnvpo  6229  cnvso  6230  xpco  6231  opreu2reurex  6236  dfpo2  6238  imaindm  6241  dflim2  6359  funcnv  6545  funcnv3  6546  fncnv  6549  fun11  6550  imadif  6560  fnres  6603  dfmpt3  6610  mptfnf  6611  fnopabg  6613  fint  6697  fin  6698  fores  6740  dff1o3  6764  f1ompt  7039  fsn  7063  imaiun  7174  isocnv2  7260  isocnv3  7261  isores2  7262  isomin  7266  eqoprab2bw  7411  eqoprab2b  7412  elpwpwel  7695  sucexb  7732  onsucb  7742  dflim4  7773  fiun  7870  f1iun  7871  f11o  7874  opabex3d  7892  opabex3rd  7893  opabex3  7894  dfopab2  7979  dfoprab3s  7980  fmpox  7994  fparlem1  8037  fparlem2  8038  tpostpos  8171  frrlem9  8219  dfsmo2  8262  brwitnlem  8417  oarec  8472  naddasslem1  8604  naddasslem2  8605  qsid  8700  uniinqs  8716  mapval2  8791  mapsncnv  8812  elixp2  8820  ixpin  8842  brsdom  8892  brdom2  8899  xpassen  8979  brsdom2  9009  unfilem1  9184  fiint  9206  dfsup2  9323  supmo  9331  eqinf  9364  infmo  9376  brttrcl2  9599  rankc1  9758  cp  9779  isinfcard  9978  aceq1  10003  aceq2  10005  dfac5lem3  10011  dfac10b  10026  dfac12a  10035  dffin7-2  10284  dfacfin7  10285  fin1a2lem6  10291  iunfo  10425  konigthlem  10454  axgroth6  10714  axgroth3  10717  sstskm  10728  ltexprlem1  10922  gt0srpr  10964  ltpsrpr  10995  map2psrpr  10996  ltresr  11026  fimaxre3  12063  sup3  12074  supaddc  12084  supmul1  12086  elnn0z  12476  elznn0nn  12477  zmin  12837  xrnemnf  13011  xrnepnf  13012  dfrp2  13289  elioomnf  13339  elxrge0  13352  elfzuzb  13413  fzass4  13457  elfz2nn0  13513  elfzo2  13557  elfzo3  13571  lbfzo0  13594  fzo1lb  13608  fzind2  13683  nn0opthlem1  14170  hashgt23el  14326  cotr2g  14878  rexfiuz  15250  fsumcom2  15676  prodmo  15838  fprodcom2  15886  sinltx  16093  divalglem4  16302  divalglem10  16308  4sqlem12  16863  imasleval  17440  xpsfrnel  17461  xpscf  17464  isssc  17722  isffth2  17820  ispos2  18216  issubmgm  18605  ismhm  18688  issubmndb  18708  nsgacs  19069  isgim  19169  oppgcntz  19271  f1omvdco3  19356  pmtrprfvalrn  19395  efgrelexlemb  19657  pgpfac1  19989  pgpfac  19993  issrg  20101  opprsubg  20265  opprunit  20290  isirred2  20334  opprirred  20335  opprnzrb  20431  isdomn2OLD  20622  opprdomnb  20627  isdomn4r  20629  drngprop  20654  opprdrng  20674  issdrg2  20705  isorng  20771  islss  20862  islbs  21005  unocv  21612  iunocv  21613  isbasis2g  22858  tgval2  22866  ntreq0  22987  isclo2  22998  cmpcov2  23300  is1stc2  23352  1stcelcls  23371  llyi  23384  unisngl  23437  txuni2  23475  xkobval  23496  hausdiag  23555  isfbas2  23745  elfg  23781  fbasrn  23794  fmfnfmlem3  23866  isfcls  23919  alexsubALTlem2  23958  istmd  23984  istgp  23987  istrg  24074  istdrg  24076  istdrg2  24088  isms2  24360  metuel2  24475  restmetu  24480  isngp  24506  isngp2  24507  isngp3  24508  elii1  24853  isncvsngp  25071  iscph  25092  isbn  25260  pmltpc  25373  ovolfcl  25389  finiunmbl  25467  iundisj  25471  dyaddisj  25519  vitalilem1  25531  ellimc3  25802  ig1pval3  26105  plyun0  26124  plydivex  26227  aannenlem2  26259  ellogrn  26490  atandm  26808  atandm3  26810  atans2  26863  elno3  27589  conway  27735  eqscut2  27742  madeval2  27789  tgjustf  28446  colinearalg  28883  axeuclid  28936  nbgrsym  29336  upgrtrls  29673  upgristrl  29674  dfpth2  29702  usgr2pth0  29738  iswwlks  29809  isclwwlk  29956  clwwlkneq0  30001  h2hlm  30952  issh  31180  chcon2i  31436  chcon1i  31437  chcon3i  31438  chnlei  31457  cmcm2i  31565  cmcm3i  31566  3oalem3  31636  pjdifnormii  31655  pjneli  31695  dfadj2  31857  cnvadj  31864  hhcno  31876  hhcnf  31877  eleigvec  31929  eleigvec2  31930  pjimai  32148  isst  32185  ishst  32186  cvnbtwn4  32261  chrelat4i  32345  2reucom  32451  reuxfrdf  32462  difrab2  32469  inpr0  32504  iunin1f  32529  disjnf  32542  cbvdisjf  32543  disjorf  32551  iundisjf  32561  disjexc  32565  xrdifh  32755  iundisjfi  32770  hashxpe  32781  pmtrprfv2  33049  xrnarchi  33145  isunit2  33199  prmidl0  33407  opprnsg  33441  ccfldextdgrr  33677  cmpcref  33855  ordtconnlem1  33929  isrrext  34005  cntnevol  34233  ddemeas  34241  omssubaddlem  34304  omssubadd  34305  eulerpartleme  34368  eulerpartlemv  34369  eulerpartlemt0  34374  eulerpartlemgvv  34381  eulerpartlemn  34386  ballotlem2  34494  ballotlemodife  34503  oddprm2  34660  bnj257  34711  bnj268  34713  bnj290  34714  bnj312  34716  bnj89  34725  bnj887  34769  bnj976  34781  bnj1019  34783  bnj1146  34795  bnj1385  34836  bnj110  34862  bnj121  34874  bnj130  34878  bnj153  34884  bnj543  34897  bnj580  34917  bnj607  34920  bnj849  34929  bnj882  34930  bnj916  34937  bnj985v  34957  bnj985  34958  bnj1033  34973  bnj1083  34982  bnj1090  34983  bnj1128  34994  bnj1174  35007  bnj1228  35015  onvf1odlem1  35139  erdszelem1  35227  cvmliftlem15  35334  snmlval  35367  satfvsuclem2  35396  satfdm  35405  elmpst  35572  mpstrcl  35577  orbi2iALT  35721  untuni  35745  dfso3  35756  xpab  35762  dftr6  35787  coep  35788  coepr  35789  dffr5  35790  dfso2  35791  cnvco1  35795  cnvco2  35796  eldm3  35797  dfdm5  35809  dfrn5  35810  brsset  35923  idsset  35924  dfon3  35926  dfbigcup2  35933  dfom5b  35946  dffun10  35948  dfiota3  35957  fnimage  35963  brdomain  35967  brrange  35968  brimg  35971  brapply  35972  brcup  35973  brcap  35974  brsuccf  35975  funpartlem  35976  brrestrict  35983  dfrecs2  35984  brub  35988  altopelaltxp  36010  rmoeqi  36221  rmoeqbii  36222  reueqi  36223  reueqbii  36224  sbceqbii  36225  disjeq1i  36226  cbvralvw2  36260  cbvrexvw2  36261  cbvrmovw2  36262  cbvreuvw2  36263  cbvsbcvw2  36264  cbvdisjvw2  36269  trer  36350  filnetlem4  36415  df3nandALT1  36433  imnand2  36436  bj-dfbi5  36608  bj-bixor  36625  bj-nnfnt  36774  bj-csbsnlem  36937  bj-rcleqf  37059  bj-sscon  37063  bj-pw0ALT  37083  bj-restpw  37126  bj-opelidb1  37187  bj-imdiridlem  37219  bj-imdirco  37224  wl-df3xor2  37503  wl-3xorrot  37511  wl-3xorcoma  37512  wl-3xornot  37515  wl-df2-3mintru2  37519  wl-df3-3mintru2  37520  wl-df4-3mintru2  37521  wl-equsalvw  37572  wl-sb9v  37583  iundif1  37634  poimirlem25  37685  poimirlem26  37686  poimirlem30  37690  ismblfin  37701  mbfposadd  37707  itg2addnclem2  37712  ftc1anc  37741  inixp  37768  prdstotbnd  37834  heibor1lem  37849  isrngohom  38005  isidl  38054  isfldidl2  38109  isdmn3  38114  sbccom2lem  38164  triantru3  38264  vvdifopab  38295  brres2  38303  eldmqsres  38321  inxpss  38345  ref5  38347  n0el2  38363  trcoss2  38521  dfeqvrel2  38627  dfeqvrel3  38628  redundeq1  38666  redundpbi1  38668  refrelredund4  38672  funALTVfun  38736  dfeldisj3  38757  dfeldisj5  38759  pet0  38853  petid  38855  petidres  38857  petinidres  38859  petxrnidres  38861  mpet  38877  petincnvepres  38887  pet  38889  pmapglbx  39808  lhpexle3  40051  cdleme25cv  40397  dicelval3  41219  diclspsn  41233  lcfls1c  41575  sn-axrep5v  42249  sn-iotalem  42254  psspwb  42261  redvmptabs  42393  eu6w  42709  moxfr  42725  fphpd  42849  uniel  43250  dflim6  43297  onsucf1olem  43303  dflim7  43306  omge2  43331  oenassex  43351  safesnsupfilb  43451  ifpim1  43502  ifpnot  43503  ifpid2  43504  ifpim2  43505  ifpxorcor  43509  ifpnot23  43511  ifpananb  43539  ifpnannanb  43540  ifpxorxorb  43544  rp-fakeinunass  43548  snen1g  43557  pren2  43586  alephiso2  43591  undmrnresiss  43637  cnvssco  43639  cotrintab  43647  cnviun  43683  imaiun1  43684  coiun1  43685  elintima  43686  frege133d  43798  frege54cor0a  43896  or3or  44056  andi3or  44057  ntrneik4w  44133  k0004lem1  44180  ismnuprim  44327  ismnushort  44334  undisjrab  44339  nzss  44350  pm10.541  44400  compab  44474  onfrALTlem5  44575  onfrALTlem5VD  44917  rext0  44971  wfaxun  45032  brpermmodel  45036  permaxrep  45039  permaxpow  45042  permac8prim  45047  eluni2f  45140  euabsneu  47059  aiotaexb  47120  aiotavb  47121  r19.32  47129  3an4ancom24  47300  ichn  47487  ichcom  47490  ichbi12i  47491  prproropf1olem0  47533  pairreueq  47541  clnbgrsym  47869  usgrexmpl2nb0  48062  usgrexmpl2nb1  48063  usgrexmpl2nb2  48064  usgrexmpl2nb3  48065  usgrexmpl2nb4  48066  usgrexmpl2nb5  48067  sgrp2sgrp  48259  islindeps  48485  elbigo  48583  reutruALT  48836  coxp  48864  tposres0  48908  catcinv  49431  isthincd2  49469  setrec1lem3  49721  elpg  49746