Theorem 3bitr4i 295

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

Syntax hints:   ↔ wb 198

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 199

This theorem is referenced by:  bibi2d  335  pm4.71  550  pm5.32ri  568  an31  635  an4  643  pm4.14  794  or4  910  orimdi  914  orbidi  935  ordi  988  ordir  989  andir  991  dfbi3  1030  dfifp7  1050  ifpn  1053  3orrot  1073  3orcoma  1074  3ioran  1086  3ianor  1087  3anbi123i  1135  3orbi123i  1136  an6  1424  3or6  1426  an33rean  1462  nancom  1468  xorcom  1491  xorass  1492  xorbi12i  1501  anxordi  1503  hadbi  1561  hadcoma  1562  hadcomb  1563  hadnot  1565  cador  1571  cadan  1572  cadcoma  1575  cadnot  1578  nic-axALT  1637  nfnbi  1817  19.26-3an  1835  19.43OLD  1846  19.32v  1899  19.31v  1900  19.42v  1912  4exdistr  1921  cbvexvw  1993  sbcom3vv  2040  excom  2096  19.32  2163  19.31  2164  19.42  2167  equsalv  2194  sbor  2238  sbbi  2239  sbnvOLD  2243  sbanvOLD  2247  sbbivOLD  2248  cbvexv1  2276  eeeanv  2282  sbnf2  2289  cbvex2  2345  equsal  2350  sbcom4  2412  dfsb3  2452  sbanOLD  2463  sbal  2496  sbex  2498  dfsb3ALT  2516  sbanALT  2534  sbbiALT  2535  eu6  2585  dfeu  2607  sb8eulem  2626  sb8mo  2629  cbveuALT  2632  cbvmoOLD  2633  eu1  2635  eu1OLD  2636  sbmo  2642  abeq1  2892  cbvabv  2904  cbvab  2905  nfceqi  2922  sbabel  2960  ralbii2  3107  r19.21v  3119  r2allem  3144  ralcom4  3176  rexbii2  3186  rexanidOLD  3193  reuanid  3263  rmoanid  3264  r19.30OLD  3274  r19.32v  3275  r19.41v  3282  r19.41  3283  r19.42v  3285  r19.43  3286  ralcom  3289  rexcomOLD  3291  ralcomf  3292  rexcomf  3293  reeanlem  3300  3reeanv  3303  2ralor  3304  rabid2  3314  rabid2f  3315  rabbi  3316  reubiia  3324  rmobiia  3329  reu5  3364  rmo5  3368  cbvralf  3371  cbvrexf  3372  cbvreu  3375  cbvrmo  3376  vjust  3410  abv  3419  ceqsex3v  3460  ceqsex4v  3461  ceqsex8v  3463  eueq  3607  eueqOLD  3608  reu2  3624  reu6  3625  reu3  3626  rmo4  3629  rmo3f  3633  2reu5  3654  cbvsbc  3706  sbccomlem  3752  rmo3  3771  rmo3OLD  3772  rmoanim  3777  rmoanimALT  3778  cbvralcsf  3816  cbvrexcsf  3817  cbvreucsf  3818  eqss  3869  uniiunlem  3947  sspsstri  3965  compleq  4009  ssequn1  4040  unss  4044  rexun  4050  ralunb  4051  elin3  4061  incom  4062  inass  4078  ssin  4089  elsymdif  4106  nssinpss  4115  dfun2  4118  difin  4120  indi  4132  indifdir  4142  ssdif0  4204  inssdif0  4210  rabeq0  4219  disj3  4280  ssundif  4310  dfif2  4346  eldifpr  4463  rexsns  4475  snprc  4521  reusn  4531  difsnpss  4608  tpss  4636  pwpr  4700  eluni2  4710  elunirab  4718  uniun  4725  unissb  4737  elintrab  4755  ssintrab  4766  intun  4775  intpr  4776  iuncom  4793  iuncom4  4794  iunab  4835  ssiinf  4838  iunn0  4849  iinab  4850  iunin2  4853  iinun2  4855  iundif2  4856  iunun  4875  iunxun  4876  iunxiun  4879  sspwuni  4882  iinpw  4888  cbvdisj  4901  disjor  4905  brun  4974  brin  4975  brdif  4976  dftr2  5026  intexrab  5093  inuni  5096  ssext  5197  pweqb  5199  otth2  5225  propeqop  5246  opelopabsbALT  5263  eqopab2b  5284  pwin  5299  pwun  5303  elxp2  5424  xpiundi  5465  xpiundir  5466  poinxp  5475  soinxp  5476  frinxp  5477  seinxp  5478  weinxp  5479  inopab  5544  difopab  5545  raliunxp  5553  rexiunxp  5554  rexxpf  5561  iunxpf  5562  cnvco  5599  dmiun  5624  dmuni  5625  dm0rn0  5633  dmres  5714  restidsing  5758  cnvsym  5808  asymref  5810  codir  5814  qfto  5815  cnvopab  5831  cnvdif  5836  rniun  5840  dminss  5844  imainss  5845  difxp  5855  xpdifid  5859  dmsnn0  5897  cnvcnvsn  5909  cnvresima  5920  resco  5936  imaco  5937  rnco  5938  coiun  5942  coass  5951  ressn  5968  cnviin  5969  cnvpo  5970  cnvso  5971  xpco  5972  opreu2reurex  5977  dflim2  6079  unisuc  6099  funcnv  6250  funcnv3  6251  fncnv  6254  fun11  6255  imadif  6265  fnres  6300  dfmpt3  6306  mptfnf  6307  fnopabg  6309  fint  6381  fin  6382  fores  6423  dff1o3  6444  f1ompt  6692  fsn  6714  imaiun  6823  isocnv2  6901  isocnv3  6902  isores2  6903  isomin  6907  eqoprab2b  7037  elpwpwel  7300  sucexb  7334  sucelon  7342  dflim4  7373  fun11iun  7452  f11o  7454  opabex3d  7472  opabex3  7473  dfopab2  7551  dfoprab3s  7552  fmpox  7566  fparlem1  7608  fparlem2  7609  fsplit  7613  suppvalbr  7630  tpostpos  7708  wfrlem8  7759  wfrfun  7762  dfsmo2  7781  brwitnlem  7926  oarec  7981  qsid  8155  uniinqs  8169  mapval2  8228  mapsncnv  8247  elixp2  8255  ixpin  8276  brsdom  8321  brdom2  8328  xpassen  8399  brsdom2  8429  unfilem1  8569  fiint  8582  dfsup2  8695  supmo  8703  eqinf  8735  infmo  8746  rankc1  9085  cp  9106  isinfcard  9304  aceq1  9329  aceq2  9331  dfac5lem3  9337  dfac10b  9351  dfac12a  9360  dffin7-2  9610  dfacfin7  9611  fin1a2lem6  9617  iunfo  9751  konigthlem  9780  axgroth6  10040  axgroth3  10043  sstskm  10054  ltexprlem1  10248  gt0srpr  10290  ltpsrpr  10321  map2psrpr  10322  ltresr  10352  fimaxre3  11380  sup3  11391  supaddc  11401  supmul1  11403  elnn0z  11799  elznn0nn  11800  zmin  12151  xrnemnf  12322  xrnepnf  12323  elioomnf  12641  elxrge0  12654  elfzuzb  12711  fzass4  12754  elfz2nn0  12807  elfzo2  12850  elfzo3  12863  lbfzo0  12885  fzind2  12963  nn0opthlem1  13436  cotr2g  14187  rexfiuz  14558  fsumcom2  14979  prodmo  15140  fprodcom2  15188  sinltx  15392  divalglem4  15597  divalglem10  15603  4sqlem12  16138  imasleval  16660  xpsfrnel  16682  xpscf  16685  isssc  16938  isffth2  17034  ispos2  17406  ismhm  17795  nsgacs  18089  isgim  18163  oppgcntz  18253  f1omvdco3  18328  pmtrprfvalrn  18367  efgrelexlemb  18626  pgpfac1  18942  pgpfac  18946  issrg  18970  opprsubg  19099  opprunit  19124  isirred2  19164  opprirred  19165  drngprop  19226  opprdrng  19239  issdrg2  19289  islss  19418  islbs  19560  isdomn2  19783  unocv  20516  iunocv  20517  isbasis2g  21250  tgval2  21258  ntreq0  21379  isclo2  21390  cmpcov2  21692  is1stc2  21744  1stcelcls  21763  llyi  21776  unisngl  21829  txuni2  21867  xkobval  21888  hausdiag  21947  isfbas2  22137  elfg  22173  fbasrn  22186  fmfnfmlem3  22258  isfcls  22311  alexsubALTlem2  22350  istmd  22376  istgp  22379  istrg  22465  istdrg  22467  istdrg2  22479  isms2  22753  metuel2  22868  restmetu  22873  isngp  22898  isngp2  22899  isngp3  22900  elii1  23232  isncvsngp  23446  iscph  23467  isbn  23634  pmltpc  23744  ovolfcl  23760  finiunmbl  23838  iundisj  23842  dyaddisj  23890  vitalilem1  23902  ellimc3  24170  ig1pval3  24461  plyun0  24480  plydivex  24579  aannenlem2  24611  ellogrn  24834  atandm  25145  atandm3  25147  atans2  25200  tgjustf  25951  colinearalg  26389  axeuclid  26442  nbgrsym  26838  upgrtrls  27181  upgristrl  27182  usgr2pth0  27244  iswwlks  27312  isclwwlk  27480  clwwlkneq0  27534  h2hlm  28526  issh  28754  chcon2i  29012  chcon1i  29013  chcon3i  29014  chnlei  29033  cmcm2i  29141  cmcm3i  29142  3oalem3  29212  pjdifnormii  29231  pjneli  29271  dfadj2  29433  cnvadj  29440  hhcno  29452  hhcnf  29453  eleigvec  29505  eleigvec2  29506  pjimai  29724  isst  29761  ishst  29762  cvnbtwn4  29837  chrelat4i  29921  2reucom  30015  moel  30024  difrab2  30030  iunin1f  30068  disjnf  30077  cbvdisjf  30078  disjorf  30085  iundisjf  30095  disjexc  30099  dfrp2  30232  xrdifh  30244  iundisjfi  30257  hashxpe  30265  xrnarchi  30435  isorng  30507  ccfldextdgrr  30642  pmtrprfv2  30646  cmpcref  30715  ordtconnlem1  30768  isrrext  30842  cntnevol  31089  ddemeas  31097  omssubaddlem  31159  omssubadd  31160  eulerpartleme  31223  eulerpartlemv  31224  eulerpartlemt0  31229  eulerpartlemgvv  31236  eulerpartlemn  31241  ballotlem2  31349  ballotlemodife  31358  oddprm2  31535  bnj257  31586  bnj268  31588  bnj290  31589  bnj312  31591  bnj89  31600  bnj887  31645  bnj976  31658  bnj1019  31660  bnj1146  31672  bnj1385  31713  bnj110  31738  bnj121  31750  bnj130  31754  bnj153  31760  bnj543  31773  bnj580  31793  bnj607  31796  bnj849  31805  bnj882  31806  bnj916  31813  bnj985  31833  bnj1033  31847  bnj1083  31856  bnj1090  31857  bnj1128  31868  bnj1174  31881  bnj1228  31889  erdszelem1  31983  cvmliftlem15  32090  snmlval  32123  elmpst  32243  mpstrcl  32248  untuni  32395  dfso3  32410  dftr6  32446  coep  32447  coepr  32448  dffr5  32449  dfso2  32450  dfpo2  32451  cnvco1  32455  cnvco2  32456  eldm3  32457  dfdm5  32476  dfrn5  32477  imaindm  32482  frrlem9  32592  elno3  32623  conway  32725  madeval2  32751  brsset  32811  idsset  32812  dfon3  32814  dfbigcup2  32821  dfom5b  32834  dffun10  32836  dfiota3  32845  fnimage  32851  brdomain  32855  brrange  32856  brimg  32859  brapply  32860  brcup  32861  brcap  32862  brsuccf  32863  funpartlem  32864  brrestrict  32871  dfrecs2  32872  brub  32876  altopelaltxp  32898  trer  33125  filnetlem4  33190  df3nandALT1  33208  imnand2  33211  bj-dfbi5  33362  bj-cbvex2v  33523  bj-abeq1  33546  bj-sbnf  33595  bj-csbsnlem  33652  bj-nnfnt  33713  bj-sscon  33791  bj-restpw  33828  wl-equsalvw  34156  wl-dfrexv  34238  wl-dfrexex  34239  wl-dfrmosb  34242  wl-dfrmov  34243  wl-dfreusb  34246  wl-dfreuv  34247  wl-dfrabv  34251  iundif1  34255  poimirlem25  34306  poimirlem26  34307  poimirlem30  34311  ismblfin  34322  mbfposadd  34328  itg2addnclem2  34333  ftc1anc  34364  inixp  34393  prdstotbnd  34462  heibor1lem  34477  isrngohom  34633  isidl  34682  isfldidl2  34737  isdmn3  34742  sbccom2lem  34794  triantru3  34892  vvdifopab  34913  brres2  34921  eldmqsres  34935  inxpss  34961  n0el2  34983  trcoss2  35117  dfeqvrel2  35218  dfeqvrel3  35219  redundeq1  35257  redundpbi1  35259  refrelredund4  35263  funALTVfun  35324  dfeldisj3  35345  dfeldisj5  35347  pmapglbx  36298  lhpexle3  36541  cdleme25cv  36887  dicelval3  37709  diclspsn  37723  lcfls1c  38065  psspwb  38504  moxfr  38629  fphpd  38754  ifpim1  39175  ifpnot  39176  ifpid2  39177  ifpim2  39178  ifpxorcor  39183  ifpnot23  39185  ifpananb  39213  ifpnannanb  39214  ifpxorxorb  39218  rp-fakeinunass  39222  undmrnresiss  39271  cnvssco  39273  cotrintab  39282  cnviun  39303  imaiun1  39304  coiun1  39305  elintima  39306  frege133d  39418  frege54cor0a  39517  or3or  39679  andi3or  39680  ntrneikb  39752  ntrneixb  39753  ntrneik4w  39758  k0004lem1  39805  ismnuprim  39950  undisjrab  39998  nzss  40009  pm10.541  40059  compab  40137  onfrALTlem5  40239  onfrALTlem5VD  40582  inn0f  40699  eluni2f  40738  euabsneu  42614  aiotaexb  42641  aiotavb  42642  r19.32  42648  3an4ancom24  42820  ichcom  42932  ichbi12i  42933  ichn  42936  prproropf1olem0  42972  pairreueq  42980  issubmgm  43364  sgrp2sgrp  43439  islindeps  43815  elbigo  43919  setrec1lem3  44099  elpg  44123