Theorem 3bitr4i 304

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

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  bibi2d  343  pm4.71  562  pm5.32ri  580  an31  654  pm4.14  812  or4  932  orimdi  936  orbidi  960  ordi  1013  ordir  1014  andir  1016  dfbi3  1055  dfifp7  1075  ifpdfbi  1076  ifpn  1079  3orrot  1097  3orcoma  1098  3ioran  1111  3ianor  1112  3anbi123i  1161  3orbi123i  1162  3jaob  1434  an6  1453  3or6  1455  an3andi  1490  an33rean  1491  nancom  1503  xorass  1522  anxordi  1533  norass  1544  hadbi  1605  hadcoma  1606  hadcomb  1607  hadnot  1609  cador  1615  cadan  1616  cadcoma  1619  cadnot  1622  nic-axALT  1681  19.26-3an  1879  19.43OLD  1890  19.32v  1947  19.31v  1948  19.42v  1960  4exdistr  1968  cbvexvw  2044  exexw  2060  sb3an  2092  sbcom4  2100  sbbiiev  2103  excom  2173  sbal  2180  19.32  2245  19.31  2246  19.42  2248  equsalv  2279  sbex  2292  sbrim  2315  sbor  2317  sbbi  2318  cbvex2v  2352  eeeanv  2358  sbnf2  2366  cbvsbvf  2371  cbvex2  2420  equsal  2425  dfsb3  2502  mo4  2570  eu6  2578  dfeu  2599  sb8eulem  2602  sb8mo  2605  cbvmovw  2606  cbvmow  2607  cbveuvw  2609  cbveuw  2610  cbveuALT  2612  eu1  2614  sbmo  2618  cbvabv  2809  cbvabw  2810  cbvab  2811  eqabcbw  2813  eqabcb  2879  nfceqi  2898  ralbii2  3081  rexbii2  3082  r19.26-3  3100  r19.43  3107  r2allem  3127  r19.42v  3171  r19.32v  3172  reeanlem  3210  3reeanv  3212  cbvralvw  3217  cbvrexvw  3218  ralcom  3267  ralcomf  3277  rexcomf  3278  cbvralfw  3279  cbvralsvw  3290  cbvralf  3324  cbvrexf  3325  reu5  3346  rmobiia  3350  reubiia  3351  rmo5  3362  cbvrmovw  3365  cbvreuvw  3366  cbvrmow  3369  cbvreuw  3370  cbvreu  3383  cbvrmo  3384  rabid2f  3422  abv  3443  abvALT  3444  ceqsal  3468  ceqsalv  3470  ceqsex3v  3484  ceqsex4v  3485  ceqsex8v  3487  reurab  3642  eueq  3649  reu2  3666  reu6  3667  reu3  3668  rmo4  3671  rmo3f  3675  2reu5  3699  cbvsbcw  3756  cbvsbcvw  3757  cbvsbc  3758  sbc3an  3787  sbccomlemOLD  3802  rmo3  3821  rmoanim  3826  rmoanimALT  3827  cbvralcsf  3873  cbvrexcsf  3874  cbvreucsf  3875  eqss  3930  uniiunlem  4018  sspsstri  4036  compleq  4082  ssequn1  4115  unss  4119  rexun  4125  ralunb  4126  elin3  4135  inass  4156  ssin  4167  elsymdif  4186  nssinpss  4195  dfun2  4198  difin  4200  indi  4212  indifdi  4222  difin2  4229  eq0  4278  ssdif0  4294  inn0f  4299  inssdif0  4302  ab0w  4307  ab0  4308  ab0orv  4311  abn0  4313  rabeq0w  4315  rabeq0  4316  disj3  4382  ssundif  4415  ralidmw  4444  dfif2  4456  eldifpr  4590  rexdifpr  4591  rexsns  4603  snprc  4649  reusn  4659  difsnpss  4740  tpss  4768  pwpr  4832  eluni2  4842  elunirab  4853  uniun  4861  unissb  4871  elintrab  4890  ssintrab  4901  intun  4910  iuncom  4929  iuncom4  4930  iunab  4981  ssiinf  4984  iunn0  4996  iinab  4997  iunin2  5000  iinun2  5002  iundif2  5003  iunun  5022  iunxun  5023  iunxiun  5026  sspwuni  5029  iinpw  5035  cbvdisj  5049  cbvdisjv  5050  disjor  5054  brun  5123  brin  5124  brdif  5125  dftr2  5181  dftr5  5183  intexrab  5275  inuni  5278  ssext  5393  pweqb  5395  otth2  5423  otthne  5426  propeqop  5448  vopelopabsb  5471  eqopab2bw  5490  eqopab2b  5494  pwin  5509  pwun  5511  dffr6  5574  elxp2  5642  otelxp  5662  xpiundi  5689  xpiundir  5690  poinxp  5699  soinxp  5700  frinxp  5701  seinxp  5702  weinxp  5703  reliun  5759  inopab  5772  difopab  5773  inxp  5774  raliunxp  5781  rexiunxp  5782  rexxpf  5789  iunxpf  5790  cnvco  5827  dmiun  5855  dmuni  5856  dm0rn0  5866  dm0rn0OLD  5867  dmres  5964  restidsing  6005  asymref  6066  codir  6070  qfto  6071  cnvopab  6087  cnvopabOLD  6088  cnvdif  6094  rniun  6098  dminss  6104  imainss  6105  difxp  6115  xpdifid  6119  dmsnn0  6158  cnvcnvsn  6170  cnvresima  6181  resco  6201  imaco  6202  rnco  6203  rncoOLD  6204  coiun  6208  coass  6217  ressn  6236  cnviin  6237  cnvpo  6238  cnvso  6239  xpco  6240  opreu2reurex  6245  dfpo2  6247  imaindm  6250  dflim2  6368  funcnv  6554  funcnv3  6555  fncnv  6558  fun11  6559  imadif  6569  fnres  6612  dfmpt3  6619  mptfnf  6620  fnopabg  6622  fint  6706  fin  6707  fores  6749  dff1o3  6773  f1ompt  7052  fsn  7077  imaiun  7189  isocnv2  7275  isocnv3  7276  isores2  7277  isomin  7281  eqoprab2bw  7426  eqoprab2b  7427  elpwpwel  7710  sucexb  7747  onsucb  7757  dflim4  7788  fiun  7885  f1iun  7886  f11o  7889  opabex3d  7907  opabex3rd  7908  opabex3  7909  dfopab2  7994  dfoprab3s  7995  fmpox  8009  fparlem1  8051  fparlem2  8052  tpostpos  8186  frrlem9  8234  dfsmo2  8277  brwitnlem  8432  oarec  8487  naddasslem1  8620  naddasslem2  8621  qsid  8718  uniinqs  8734  mapval2  8810  mapsncnv  8831  elixp2  8839  ixpin  8861  brsdom  8911  brdom2  8919  xpassen  8999  brsdom2  9029  unfilem1  9205  fiint  9227  dfsup2  9347  supmo  9355  eqinf  9388  infmo  9400  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  20493  isdomn2OLD  20684  opprdomnb  20689  isdomn4r  20691  drngprop  20716  opprdrng  20736  issdrg2  20767  isorng  20833  islss  20924  islbs  21066  unocv  21655  iunocv  21656  isbasis2g  22931  tgval2  22939  ntreq0  23060  isclo2  23071  cmpcov2  23373  is1stc2  23425  1stcelcls  23444  llyi  23457  unisngl  23510  txuni2  23548  xkobval  23569  hausdiag  23628  isfbas2  23818  elfg  23854  fbasrn  23867  fmfnfmlem3  23939  isfcls  23992  alexsubALTlem2  24031  istmd  24057  istgp  24060  istrg  24147  istdrg  24149  istdrg2  24161  isms2  24433  metuel2  24548  restmetu  24553  isngp  24579  isngp2  24580  isngp3  24581  elii1  24920  isncvsngp  25134  iscph  25155  isbn  25323  pmltpc  25435  ovolfcl  25451  finiunmbl  25529  iundisj  25533  dyaddisj  25581  vitalilem1  25593  ellimc3  25864  ig1pval3  26161  plyun0  26180  plydivex  26281  aannenlem2  26313  ellogrn  26541  atandm  26858  atandm3  26860  atans2  26913  elno3  27637  conway  27789  eqcuts2  27796  madeval2  27843  ons2ind  28285  tgjustf  28559  colinearalg  28997  axeuclid  29050  nbgrsym  29450  upgrtrls  29786  upgristrl  29787  dfpth2  29815  usgr2pth0  29851  iswwlks  29922  isclwwlk  30072  clwwlkneq0  30117  h2hlm  31069  issh  31297  chcon2i  31553  chcon1i  31554  chcon3i  31555  chnlei  31574  cmcm2i  31682  cmcm3i  31683  3oalem3  31753  pjdifnormii  31772  pjneli  31812  dfadj2  31974  cnvadj  31981  hhcno  31993  hhcnf  31994  eleigvec  32046  eleigvec2  32047  pjimai  32265  isst  32302  ishst  32303  cvnbtwn4  32378  chrelat4i  32462  2reucom  32567  reuxfrdf  32578  difrab2  32585  inpr0  32620  iunin1f  32646  disjnf  32659  cbvdisjf  32660  disjorf  32668  iundisjf  32678  disjexc  32682  xrdifh  32872  iundisjfi  32888  hashxpe  32899  pmtrprfv2  33169  xrnarchi  33265  isunit2  33321  prmidl0  33533  opprnsg  33567  ccfldextdgrr  33856  cmpcref  34034  ordtconnlem1  34108  isrrext  34184  cntnevol  34412  ddemeas  34420  omssubaddlem  34483  omssubadd  34484  eulerpartleme  34547  eulerpartlemv  34548  eulerpartlemt0  34553  eulerpartlemgvv  34560  eulerpartlemn  34565  ballotlem2  34673  ballotlemodife  34682  oddprm2  34839  bnj257  34890  bnj268  34892  bnj290  34893  bnj312  34895  bnj89  34904  bnj887  34948  bnj976  34960  bnj1019  34962  bnj1146  34973  bnj1385  35014  bnj110  35040  bnj121  35052  bnj130  35056  bnj153  35062  bnj543  35075  bnj580  35095  bnj607  35098  bnj849  35107  bnj882  35108  bnj916  35115  bnj985v  35135  bnj985  35136  bnj1033  35151  bnj1083  35160  bnj1090  35161  bnj1128  35172  bnj1174  35185  bnj1228  35193  onvf1odlem1  35331  erdszelem1  35419  cvmliftlem15  35526  snmlval  35559  satfvsuclem2  35588  satfdm  35597  elmpst  35764  mpstrcl  35769  orbi2iALT  35913  untuni  35937  dfso3  35948  xpab  35954  dftr6  35979  coep  35980  coepr  35981  dffr5  35982  dfso2  35983  cnvco1  35987  cnvco2  35988  eldm3  35989  dfdm5  36001  dfrn5  36002  brsset  36115  idsset  36116  dfon3  36118  dfbigcup2  36125  dfom5b  36138  dffun10  36140  dfiota3  36149  fnimage  36155  brdomain  36159  brrange  36160  brimg  36163  brapply  36164  brcup  36165  brcap  36166  lemsuccf  36167  funpartlem  36170  brrestrict  36177  dfrecs2  36178  brub  36182  altopelaltxp  36204  rmoeqi  36415  rmoeqbii  36416  reueqi  36417  reueqbii  36418  sbceqbii  36419  disjeq1i  36420  cbvralvw2  36454  cbvrexvw2  36455  cbvrmovw2  36456  cbvreuvw2  36457  cbvsbcvw2  36458  cbvdisjvw2  36463  trer  36544  filnetlem4  36609  df3nandALT1  36627  imnand2  36630  mh-unprimbi  36772  bj-dfbi5  36885  bj-bixor  36902  bj-dfsbc  36992  bj-nnfnt  37093  bj-csbsnlem  37256  bj-rcleqf  37378  bj-sscon  37382  bj-pw0ALT  37402  bj-restpw  37450  bj-opelidb1  37513  bj-imdiridlem  37545  bj-imdirco  37550  wl-df3xor2  37831  wl-3xorrot  37839  wl-3xorcoma  37840  wl-3xornot  37843  wl-df2-3mintru2  37847  wl-df3-3mintru2  37848  wl-df4-3mintru2  37849  wl-equsalvw  37909  wl-sb9v  37920  iundif1  37961  poimirlem25  38012  poimirlem26  38013  poimirlem30  38017  ismblfin  38028  mbfposadd  38034  itg2addnclem2  38039  ftc1anc  38068  inixp  38095  prdstotbnd  38161  heibor1lem  38176  isrngohom  38332  isidl  38381  isfldidl2  38436  isdmn3  38441  sbccom2lem  38491  triantru3  38603  vvdifopab  38632  brres2  38640  eldmqsres  38660  inxpss  38684  ref5  38686  n0el2  38702  dfsucmap3  38830  trcoss2  38941  dfeqvrel2  39041  dfeqvrel3  39042  redundeq1  39080  redundpbi1  39082  refrelredund4  39086  funALTVfun  39150  dfeldisj3  39178  dfeldisj5  39180  pet0  39285  petid  39287  petidres  39289  petinidres  39291  petxrnidres  39293  mpet  39320  petincnvepres  39330  pet  39332  pmapglbx  40261  lhpexle3  40504  cdleme25cv  40850  dicelval3  41672  diclspsn  41686  lcfls1c  42028  sn-axrep5v  42704  sn-iotalem  42708  psspwb  42715  redvmptabs  42837  eu6w  43126  moxfr  43141  fphpd  43261  uniel  43662  dflim6  43709  onsucf1olem  43715  dflim7  43718  omge2  43743  oenassex  43763  safesnsupfilb  43862  ifpim1  43913  ifpnot  43914  ifpid2  43915  ifpim2  43916  ifpxorcor  43920  ifpnot23  43922  ifpananb  43950  ifpnannanb  43951  ifpxorxorb  43955  rp-fakeinunass  43959  snen1g  43968  pren2  43997  alephiso2  44002  undmrnresiss  44048  cnvssco  44050  cotrintab  44058  cnviun  44094  imaiun1  44095  coiun1  44096  elintima  44097  frege133d  44209  frege54cor0a  44307  or3or  44467  andi3or  44468  ntrneik4w  44544  k0004lem1  44591  ismnuprim  44738  ismnushort  44745  undisjrab  44750  nzss  44761  pm10.541  44811  compab  44885  onfrALTlem5  44986  onfrALTlem5VD  45328  rext0  45382  wfaxun  45443  brpermmodel  45447  permaxrep  45450  permaxpow  45453  permac8prim  45458  eluni2f  45550  euabsneu  47491  aiotaexb  47552  aiotavb  47553  r19.32  47561  3an4ancom24  47732  ichn  47931  ichcom  47934  ichbi12i  47935  prproropf1olem0  47977  pairreueq  47985  clnbgrsym  48329  usgrexmpl2nb0  48522  usgrexmpl2nb1  48523  usgrexmpl2nb2  48524  usgrexmpl2nb3  48525  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  sgrp2sgrp  48719  islindeps  48944  elbigo  49042  reutruALT  49295  coxp  49323  tposres0  49367  catcinv  49889  isthincd2  49927  setrec1lem3  50179  elpg  50204