Theorem 3bitr4i 306

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi2d  345  pm4.71  567  pm5.32ri  586  an31  661  pm4.14  819  or4  940  orimdi  944  orbidi  967  ordi  1023  ordir  1024  andir  1026  dfbi3  1065  dfifp7  1085  ifpdfbiOLD  1087  ifpn  1090  3orrot  1108  3orcoma  1109  3ioran  1123  3ianor  1124  3anbi123i  1173  3orbi123i  1174  3jaob  1453  an6  1474  3or6  1476  an3andi  1513  an33rean  1514  nancom  1526  xorass  1545  anxordi  1556  norass  1567  hadbi  1628  hadcoma  1629  hadcomb  1630  hadnot  1632  cador  1641  cadan  1642  cadcoma  1645  cadnot  1648  nic-axALT  1707  19.26-3an  1905  19.43OLD  1916  19.32v  1973  19.31v  1974  19.42v  1986  4exdistr  1994  cbvexvw  2070  exexw  2086  sb3an  2118  sbcom4  2126  sbbiiev  2130  excom  2199  sbal  2206  19.32  2270  19.31  2271  19.42  2273  equsalv  2302  sbex  2315  sbrim  2338  sbor  2340  sbbi  2341  cbvex2v  2374  eeeanv  2380  sbnf2  2388  cbvsbvf  2393  cbvex2  2442  equsal  2447  dfsb3  2524  mo4  2592  eu6  2600  dfeu  2621  sb8eulem  2624  sb8mo  2627  cbvmovw  2628  cbvmow  2629  cbveuvw  2631  cbveuw  2632  cbveuALT  2634  eu1  2636  sbmo  2640  cbvabv  2831  cbvabw  2832  cbvab  2833  eqabcbw  2835  eqabcb  2901  nfceqi  2920  ralbii2  3105  rexbii2  3106  r19.26-3  3124  r19.43  3131  r2allem  3151  r19.42v  3195  r19.32v  3196  reeanlem  3234  3reeanv  3236  cbvralvw  3241  cbvrexvw  3242  ralcom  3291  ralcomf  3301  rexcomf  3302  cbvralfw  3303  cbvralsvw  3314  cbvralf  3346  cbvrexf  3347  reu5  3368  rmobiia  3372  reubiia  3373  rmo5  3384  cbvrmovw  3387  cbvreuvw  3388  cbvrmow  3391  cbvreuw  3392  cbvreu  3405  cbvrmo  3406  rabid2f  3443  abv  3463  abvALT  3464  ceqsal  3488  ceqsalv  3490  ceqsex3v  3503  ceqsex4v  3504  ceqsex8v  3506  reurab  3659  eueq  3666  reu2  3683  reu6  3684  reu3  3685  rmo4  3688  rmo3f  3692  2reu5  3716  cbvsbcw  3772  cbvsbcvw  3773  cbvsbc  3774  sbc3an  3803  rmo3  3836  rmoanim  3842  rmoanimALT  3843  cbvralcsf  3889  cbvrexcsf  3890  cbvreucsf  3891  eqss  3946  uniiunlem  4035  sspsstri  4054  compleq  4099  ssequn1  4132  unss  4136  rexun  4142  ralunb  4143  elin3  4152  inass  4173  ssin  4184  elsymdif  4204  nssinpss  4213  dfun2  4216  difin  4218  indi  4230  indifdi  4240  difin2  4247  eq0  4297  ssdif0  4314  inn0f  4319  inssdif0OLD  4323  ab0w  4328  ab0  4329  ab0orv  4332  abn0  4334  rabeq0w  4337  rabeq0  4338  disj3  4407  ssundif  4443  ralidmw  4472  dfif2  4484  eldifpr  4619  rexdifpr  4620  rexsns  4632  snprc  4678  reusn  4688  difsnpss  4770  tpss  4797  pwpr  4861  eluni2  4871  elunirab  4882  uniun  4890  unissb  4901  elintrab  4920  ssintrab  4931  intun  4940  iuncom  4959  iuncom4  4960  iunab  5010  ssiinf  5013  iunn0  5025  iinab  5026  iunin2  5029  iinun2  5031  iundif2  5032  iunun  5053  iunxun  5054  iunxiun  5057  sspwuni  5060  iinpw  5066  cbvdisj  5080  cbvdisjv  5081  disjor  5085  brun  5156  brin  5157  brdif  5158  dftr2  5214  dftr5  5216  intexrab  5308  inuni  5311  ssext  5422  pweqb  5424  otth2  5452  otthne  5455  propeqop  5479  vopelopabsb  5503  eqopab2bw  5523  eqopab2b  5527  pwin  5542  pwun  5544  dffr6  5607  elxp2  5675  otelxp  5695  xpiundi  5722  xpiundir  5723  poinxp  5732  soinxp  5733  frinxp  5734  seinxp  5735  weinxp  5736  reliun  5794  inopab  5807  difopab  5808  inxp  5809  raliunxp  5816  rexiunxp  5817  rexxpf  5825  iunxpf  5826  cnvco  5867  dmiun  5895  dmuni  5896  dm0rn0  5906  dm0rn0OLD  5907  dmres  6003  restidsing  6045  asymref  6110  codir  6114  qfto  6115  cnvopab  6131  cnvdif  6134  rniun  6139  dminss  6143  imainss  6144  cnvxp  6147  difxp  6155  xpdifid  6159  xpdifcnvepel  6160  dmsnn0  6207  cnvcnvsn  6219  cnvresima  6230  resco  6250  imaco  6251  rnco  6252  rncoOLD  6253  coiun  6257  coass  6266  ressn  6287  cnviin  6288  cnvpo  6289  cnvso  6290  xpco  6291  opreu2reurex  6296  dfpo2  6298  imaindm  6301  dflim2  6420  funcnv  6607  funcnv3  6608  fncnv  6611  fun11  6612  imadif  6622  fnres  6664  dfmpt3  6671  mptfnf  6672  fnopabg  6674  fint  6759  fin  6760  fores  6804  dff1o3  6829  f1ompt  7109  fsn  7134  imaiun  7247  isocnv2  7337  isocnv3  7338  isores2  7339  isomin  7343  eqoprab2bw  7488  eqoprab2b  7489  elpwpwel  7779  sucexb  7816  onsucb  7826  dflim4  7857  fiun  7953  f1iun  7954  f11o  7957  opabex3d  7975  opabex3rd  7976  opabex3  7977  dfopab2  8061  dfoprab3s  8062  fmpox  8076  fparlem1  8121  fparlem2  8122  tpostpos  8256  frrlem9  8305  dfsmo2  8348  brwitnlem  8508  oarec  8563  naddasslem1  8697  naddasslem2  8698  qsid  8795  uniinqs  8811  mapval2  8893  mapsncnv  8914  elixp2  8922  ixpin  8944  brsdom  8994  brdom2  9002  xpassen  9083  brsdom2  9113  unfilem1  9290  fiint  9311  dfsup2  9429  supmo  9437  eqinf  9470  infmo  9482  brttrcl2  9708  rankc1  9880  cp  9947  setrec1lem3  9962  isinfcard  10164  aceq1  10189  aceq2  10191  dfac5lem3  10197  dfac10b  10211  dfac12a  10220  dffin7-2  10469  dfacfin7  10470  fin1a2lem6  10476  iunfo  10616  konigthlem  10646  axgroth6  10906  axgroth3  10909  sstskm  10920  ltexprlem1  11114  gt0srpr  11156  ltpsrpr  11187  map2psrpr  11188  ltresr  11218  fimaxre3  12256  sup3  12267  supaddc  12277  supmul1  12279  elnn0z  12699  elznn0nn  12700  zmin  13064  xrnemnf  13239  xrnepnf  13240  dfrp2  13518  elioomnf  13568  elxrge0  13581  elfzuzb  13643  fzass4  13689  elfz2nn0  13745  elfzo2  13789  elfzo3  13804  lbfzo0  13827  fzo1lb  13841  fzind2  13916  nn0opthlem1  14405  hashgt23el  14562  cotr2g  15122  rexfiuz  15508  fsumcom2  15933  prodmo  16096  fprodcom2  16144  sinltx  16350  divalglem4  16559  divalglem10  16565  4sqlem12  17127  imasleval  17706  xpsfrnel  17727  xpscf  17730  isssc  17988  isffth2  18086  ispos2  18482  issubmgm  18884  ismhm  18973  issubmndb  18993  nsgacs  19365  isgim  19469  oppgcntz  19571  f1omvdco3  19656  pmtrprfvalrn  19695  efgrelexlemb  19957  pgpfac1  20289  pgpfac  20293  issrg  20407  dfring3  20511  opprsubg  20575  opprunit  20600  isirred2  20644  opprirred  20645  isrhm0  20699  dfric2  20750  opprnzrb  20765  opprdomnb  20961  isdomn4r  20963  drngprop  20991  isdrng3  21000  isdrng5  21001  opprdrng  21014  issdrg2  21045  isorng  21111  islss  21202  islbs  21344  isfieldidl  21533  isfieldidl2  21534  prmidl0  21627  unocv  21979  iunocv  21980  isbasis2g  23259  tgval2  23267  ntreq0  23388  isclo2  23399  cmpcov2  23701  is1stc2  23753  1stcelcls  23773  llyi  23786  unisngl  23839  txuni2  23877  xkobval  23898  hausdiag  23957  isfbas2  24147  elfg  24183  fbasrn  24196  fmfnfmlem3  24268  isfcls  24321  alexsubALTlem2  24360  istmd  24386  istgp  24389  istrg  24476  istdrg  24478  istdrg2  24490  isms2  24762  metuel2  24877  restmetu  24882  isngp  24908  isngp2  24909  isngp3  24910  elii1  25249  isncvsngp  25463  iscph  25484  isbn  25652  pmltpc  25764  ovolfcl  25780  finiunmbl  25858  iundisj  25862  dyaddisj  25910  vitalilem1  25922  ellimc3  26192  ig1pval3  26489  plyun0  26508  plydivex  26611  aannenlem2  26649  ellogrn  26880  atandm  27197  atandm3  27199  atans2  27252  elno3  28005  conway  28158  eqcuts2  28165  madeval2  28212  ons2ind  28654  tgjustf  28928  colinearalg  29481  axeuclid  29534  nbgrsym  29937  upgrtrls  30277  upgristrl  30278  dfpth2  30307  usgr2pth0  30344  iswwlks  30418  isclwwlk  30568  clwwlkneq0  30613  h2hlm  31575  issh  31803  chcon2i  32059  chcon1i  32060  chcon3i  32061  chnlei  32080  cmcm2i  32188  cmcm3i  32189  3oalem3  32259  pjdifnormii  32278  pjneli  32318  dfadj2  32480  cnvadj  32487  hhcno  32499  hhcnf  32500  eleigvec  32552  eleigvec2  32553  pjimai  32771  isst  32808  ishst  32809  cvnbtwn4  32884  chrelat4i  32968  2reucom  33069  reuxfrdf  33080  difrab2  33087  inpr0  33121  iunin1f  33145  disjnf  33157  cbvdisjf  33158  disjorf  33166  iundisjf  33176  disjexc  33180  xrdifh  33365  iundisjfi  33381  hashxpe  33392  pmtrprfv2  33642  xrnarchi  33738  isunit2  33793  opprnsg  34001  ccfldextdgrr  34297  cmpcref  34475  ordtconnlem1  34549  isrrext  34625  cntnevol  34854  ddemeas  34862  omssubaddlem  34924  omssubadd  34925  eulerpartleme  34988  eulerpartlemv  34989  eulerpartlemt0  34994  eulerpartlemgvv  35001  eulerpartlemn  35006  ballotlem2  35114  ballotlemodife  35123  oddprm2  35277  bnj257  35331  bnj268  35333  bnj290  35334  bnj312  35336  bnj89  35345  bnj887  35389  bnj976  35401  bnj1019  35403  bnj1146  35414  bnj1385  35455  bnj110  35481  bnj121  35493  bnj130  35497  bnj153  35503  bnj543  35516  bnj580  35536  bnj607  35539  bnj849  35548  bnj882  35549  bnj916  35556  bnj985v  35576  bnj985  35577  bnj1033  35592  bnj1083  35601  bnj1090  35602  bnj1128  35613  bnj1174  35626  bnj1228  35634  onvf1odlem1  35865  erdszelem1  35935  cvmliftlem15  36042  snmlval  36075  satfvsuclem2  36104  satfdm  36113  elmpst  36280  mpstrcl  36285  orbi2iALT  36429  untuni  36453  dfso3  36464  xpab  36470  dftr6  36495  coep  36496  coepr  36497  dffr5  36498  dfso2  36499  cnvco1  36503  cnvco2  36504  eldm3  36505  dfdm5  36517  dfrn5  36518  brsset  36631  idsset  36632  dfon3  36634  dfbigcup2  36641  dfom5b  36654  dffun10  36656  dfiota3  36665  fnimage  36671  brdomain  36675  brrange  36676  brimg  36679  brapply  36680  brcup  36681  brcap  36682  lemsuccf  36683  funpartlem  36686  brrestrict  36693  dfrecs2  36694  brub  36698  dffr7  36700  altopelaltxp  36721  ltnadd  36947  rmoeqi  36956  rmoeqbii  36957  reueqi  36958  reueqbii  36959  sbceqbii  36960  disjeq1i  36961  cbvralvw2  36995  cbvrexvw2  36996  cbvrmovw2  36997  cbvreuvw2  36998  cbvsbcvw2  36999  cbvdisjvw2  37004  trer  37084  filnetlem4  37149  df3nandALT1  37167  imnand2  37170  mh-unprimbi  37312  bj-dfbi5  37424  bj-bixor  37441  bj-dfsbc  37531  bj-nnfnt  37632  bj-csbsnlem  37795  bj-rcleqf  37918  bj-sscon  37922  coi1in  37941  bj-pw0ALT  37944  bj-restpw  37993  bj-opelidb1  38054  bj-imdiridlem  38086  bj-imdirco  38091  wl-df3xor2  38372  wl-3xorrot  38380  wl-3xorcoma  38381  wl-3xornot  38384  wl-df2-3mintru2  38388  wl-df3-3mintru2  38389  wl-df4-3mintru2  38390  wl-equsalvw  38450  wl-sb9v  38461  iundif1  38502  poimirlem25  38543  poimirlem26  38544  poimirlem30  38548  ismblfin  38559  mbfposadd  38565  itg2addnclem2  38570  ftc1anc  38599  inixp  38642  prdstotbnd  38708  heibor1lem  38723  isrngohom  38879  isidl  38928  isfldidl2  38983  isdmn3  38988  sbccom2lem  39036  scott0f  39081  triantru3  39148  vvdifopab  39177  brres2  39185  eldmqsres  39205  inxpss  39229  ref5  39231  n0el2  39247  dfsucmap3  39375  trcoss2  39486  dfeqvrel2  39586  dfeqvrel3  39587  redundeq1  39625  redundpbi1  39627  refrelredund4  39631  funALTVfun  39695  dfeldisj3  39723  dfeldisj5  39725  pet0  39830  petid  39832  petidres  39834  petinidres  39836  petxrnidres  39838  mpet  39865  petincnvepres  39875  pet  39877  pmapglbx  40806  lhpexle3  41049  cdleme25cv  41395  dicelval3  42217  diclspsn  42231  lcfls1c  42573  sn-axrep5v  43251  sn-iotalem  43255  psspwb  43262  redvmptabs  43391  eu6w  43667  moxfr  43682  fphpd  43802  uniel  44203  dflim6  44250  onsucf1olem  44256  dflim7  44259  omge2  44284  oenassex  44304  safesnsupfilb  44403  ifpim1  44454  ifpnot  44455  ifpid2  44456  ifpim2  44457  ifpxorcor  44461  ifpnot23  44463  ifpananb  44491  ifpnannanb  44492  ifpxorxorb  44496  rp-fakeinunass  44500  snen1g  44509  pren2  44538  alephiso2  44543  undmrnresiss  44589  cnvssco  44591  cotrintab  44599  cnviun  44635  imaiun1  44636  coiun1  44637  elintima  44638  frege133d  44750  frege54cor0a  44848  or3or  45008  andi3or  45009  ntrneik4w  45085  k0004lem1  45132  ismnuprim  45263  ismnushort  45270  undisjrab  45275  nzss  45286  pm10.541  45336  compab  45410  onfrALTlem5  45510  onfrALTlem5VD  45852  rext0  45906  wfaxun  45967  brpermmodel  45971  permaxrep  45974  permaxpow  45977  permac8prim  45982  eluni2f  46087  euabsneu  48067  aiotaexb  48128  aiotavb  48129  r19.32  48137  3an4ancom24  48308  ichn  48507  ichcom  48510  ichbi12i  48511  prproropf1olem0  48553  pairreueq  48561  clnbgrsym  48905  usgrexmpl2nb0  49098  usgrexmpl2nb1  49099  usgrexmpl2nb2  49100  usgrexmpl2nb3  49101  usgrexmpl2nb4  49102  usgrexmpl2nb5  49103  sgrp2sgrp  49294  isidom3  49411  islindeps  49534  elbigo  49632  reutruALT  49884  coxp  49912  tposres0  49954  catcinv  50476  isthincd2  50514  elpg  50776  dfrals2  50855  alsbii  50865  ralsbii  50866  cbvals  50870  dfralseu2  50888  alseubii  50897  ralseubii  50898