Theorem 3bitr4i 305

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  bibi2d  344  pm4.71  565  pm5.32ri  583  an31  658  pm4.14  816  or4  937  orimdi  941  orbidi  965  ordi  1019  ordir  1020  andir  1022  dfbi3  1061  dfifp7  1081  ifpdfbi  1082  ifpn  1085  3orrot  1103  3orcoma  1104  3ioran  1118  3ianor  1119  3anbi123i  1168  3orbi123i  1169  3jaob  1445  an6  1466  3or6  1468  an3andi  1503  an33rean  1504  nancom  1516  xorass  1535  anxordi  1546  norass  1557  hadbi  1618  hadcoma  1619  hadcomb  1620  hadnot  1622  cador  1628  cadan  1629  cadcoma  1632  cadnot  1635  nic-axALT  1694  19.26-3an  1892  19.43OLD  1903  19.32v  1960  19.31v  1961  19.42v  1973  4exdistr  1981  cbvexvw  2057  exexw  2073  sb3an  2114  sbcom4  2122  sbbiiev  2126  excom  2196  sbal  2203  19.32  2268  19.31  2269  19.42  2271  equsalv  2302  sbex  2315  sbrim  2338  sbor  2340  sbbi  2341  cbvex2v  2375  eeeanv  2381  sbnf2  2389  cbvsbvf  2394  cbvex2  2443  equsal  2448  dfsb3  2525  mo4  2593  eu6  2601  dfeu  2622  sb8eulem  2625  sb8mo  2628  cbvmovw  2629  cbvmow  2630  cbveuvw  2632  cbveuw  2633  cbveuALT  2635  eu1  2637  sbmo  2641  cbvabv  2832  cbvabw  2833  cbvab  2834  eqabcbw  2836  eqabcb  2902  nfceqi  2921  ralbii2  3104  rexbii2  3105  r19.26-3  3123  r19.43  3130  r2allem  3150  r19.42v  3194  r19.32v  3195  reeanlem  3233  3reeanv  3235  cbvralvw  3240  cbvrexvw  3241  ralcom  3290  ralcomf  3300  rexcomf  3301  cbvralfw  3302  cbvralsvw  3313  cbvralf  3347  cbvrexf  3348  reu5  3369  rmobiia  3373  reubiia  3374  rmo5  3385  cbvrmovw  3388  cbvreuvw  3389  cbvrmow  3392  cbvreuw  3393  cbvreu  3406  cbvrmo  3407  rabid2f  3445  abv  3466  abvALT  3467  ceqsal  3491  ceqsalv  3493  ceqsex3v  3506  ceqsex4v  3507  ceqsex8v  3509  reurab  3664  eueq  3671  reu2  3688  reu6  3689  reu3  3690  rmo4  3693  rmo3f  3697  2reu5  3721  cbvsbcw  3777  cbvsbcvw  3778  cbvsbc  3779  sbc3an  3808  sbccomlemOLD  3823  rmo3  3842  rmoanim  3847  rmoanimALT  3848  cbvralcsf  3894  cbvrexcsf  3895  cbvreucsf  3896  eqss  3951  uniiunlem  4040  sspsstri  4059  compleq  4105  ssequn1  4138  unss  4142  rexun  4148  ralunb  4149  elin3  4158  inass  4179  ssin  4190  elsymdif  4210  nssinpss  4219  dfun2  4222  difin  4224  indi  4236  indifdi  4246  difin2  4253  eq0  4302  ssdif0  4319  inn0f  4324  inssdif0  4327  ab0w  4332  ab0  4333  ab0orv  4336  abn0  4338  rabeq0w  4341  rabeq0  4342  disj3  4408  ssundif  4441  ralidmw  4470  dfif2  4482  eldifpr  4617  rexdifpr  4618  rexsns  4630  snprc  4676  reusn  4686  difsnpss  4767  tpss  4795  pwpr  4859  eluni2  4869  elunirab  4880  uniun  4888  unissb  4899  elintrab  4918  ssintrab  4929  intun  4938  iuncom  4957  iuncom4  4958  iunab  5009  ssiinf  5012  iunn0  5024  iinab  5025  iunin2  5028  iinun2  5030  iundif2  5031  iunun  5050  iunxun  5051  iunxiun  5054  sspwuni  5057  iinpw  5063  cbvdisj  5077  cbvdisjv  5078  disjor  5082  brun  5151  brin  5152  brdif  5153  dftr2  5209  dftr5  5211  intexrab  5303  inuni  5306  ssext  5421  pweqb  5423  otth2  5451  otthne  5454  propeqop  5476  vopelopabsb  5499  eqopab2bw  5519  eqopab2b  5523  pwin  5538  pwun  5540  dffr6  5603  elxp2  5671  otelxp  5691  xpiundi  5718  xpiundir  5719  poinxp  5728  soinxp  5729  frinxp  5730  seinxp  5731  weinxp  5732  reliun  5789  inopab  5802  difopab  5803  inxp  5804  raliunxp  5811  rexiunxp  5812  rexxpf  5819  iunxpf  5820  cnvco  5861  dmiun  5889  dmuni  5890  dm0rn0  5900  dm0rn0OLD  5901  dmres  5998  restidsing  6042  asymref  6103  codir  6107  qfto  6108  cnvopab  6124  cnvdif  6127  rniun  6132  dminss  6138  imainss  6139  difxp  6149  xpdifid  6153  xpdifcnvepel  6154  dmsnn0  6194  cnvcnvsn  6206  cnvresima  6217  resco  6237  imaco  6238  rnco  6239  rncoOLD  6240  coiun  6244  coass  6253  ressn  6272  cnviin  6273  cnvpo  6274  cnvso  6275  xpco  6276  opreu2reurex  6281  dfpo2  6283  imaindm  6286  dflim2  6404  funcnv  6590  funcnv3  6591  fncnv  6594  fun11  6595  imadif  6605  fnres  6648  dfmpt3  6655  mptfnf  6656  fnopabg  6658  fint  6743  fin  6744  fores  6788  dff1o3  6813  f1ompt  7092  fsn  7117  imaiun  7229  isocnv2  7315  isocnv3  7316  isores2  7317  isomin  7321  eqoprab2bw  7466  eqoprab2b  7467  elpwpwel  7750  sucexb  7787  onsucb  7797  dflim4  7828  fiun  7924  f1iun  7925  f11o  7928  opabex3d  7946  opabex3rd  7947  opabex3  7948  dfopab2  8033  dfoprab3s  8034  fmpox  8048  fparlem1  8091  fparlem2  8092  tpostpos  8226  frrlem9  8275  dfsmo2  8318  brwitnlem  8476  oarec  8531  naddasslem1  8665  naddasslem2  8666  qsid  8763  uniinqs  8779  mapval2  8854  mapsncnv  8875  elixp2  8883  ixpin  8905  brsdom  8955  brdom2  8963  xpassen  9043  brsdom2  9073  unfilem1  9249  fiint  9271  dfsup2  9390  supmo  9398  eqinf  9431  infmo  9443  brttrcl2  9669  rankc1  9828  cp  9849  isinfcard  10048  aceq1  10073  aceq2  10075  dfac5lem3  10081  dfac10b  10096  dfac12a  10105  dffin7-2  10355  dfacfin7  10356  fin1a2lem6  10362  iunfo  10496  konigthlem  10526  axgroth6  10786  axgroth3  10789  sstskm  10800  ltexprlem1  10994  gt0srpr  11036  ltpsrpr  11067  map2psrpr  11068  ltresr  11098  fimaxre3  12138  sup3  12149  supaddc  12159  supmul1  12161  elnn0z  12581  elznn0nn  12582  zmin  12945  xrnemnf  13119  xrnepnf  13120  dfrp2  13398  elioomnf  13448  elxrge0  13461  elfzuzb  13523  fzass4  13567  elfz2nn0  13623  elfzo2  13667  elfzo3  13682  lbfzo0  13705  fzo1lb  13719  fzind2  13794  nn0opthlem1  14281  hashgt23el  14437  cotr2g  14989  rexfiuz  15375  fsumcom2  15801  prodmo  15966  fprodcom2  16014  sinltx  16221  divalglem4  16430  divalglem10  16436  4sqlem12  16992  imasleval  17571  xpsfrnel  17592  xpscf  17595  isssc  17853  isffth2  17951  ispos2  18347  issubmgm  18736  ismhm  18819  issubmndb  18839  nsgacs  19203  isgim  19302  oppgcntz  19404  f1omvdco3  19489  pmtrprfvalrn  19528  efgrelexlemb  19790  pgpfac1  20122  pgpfac  20126  issrg  20234  opprsubg  20397  opprunit  20422  isirred2  20466  opprirred  20467  opprnzrb  20567  isdomn2OLD  20758  opprdomnb  20763  isdomn4r  20765  drngprop  20790  opprdrng  20810  issdrg2  20841  isorng  20907  islss  20998  islbs  21140  unocv  21729  iunocv  21730  isbasis2g  23005  tgval2  23013  ntreq0  23134  isclo2  23145  cmpcov2  23447  is1stc2  23499  1stcelcls  23518  llyi  23531  unisngl  23584  txuni2  23622  xkobval  23643  hausdiag  23702  isfbas2  23892  elfg  23928  fbasrn  23941  fmfnfmlem3  24013  isfcls  24066  alexsubALTlem2  24105  istmd  24131  istgp  24134  istrg  24221  istdrg  24223  istdrg2  24235  isms2  24507  metuel2  24622  restmetu  24627  isngp  24653  isngp2  24654  isngp3  24655  elii1  24994  isncvsngp  25208  iscph  25229  isbn  25397  pmltpc  25509  ovolfcl  25525  finiunmbl  25603  iundisj  25607  dyaddisj  25655  vitalilem1  25667  ellimc3  25938  ig1pval3  26235  plyun0  26254  plydivex  26358  aannenlem2  26390  ellogrn  26621  atandm  26938  atandm3  26940  atans2  26993  elno3  27716  conway  27869  eqcuts2  27876  madeval2  27923  ons2ind  28365  tgjustf  28639  colinearalg  29108  axeuclid  29161  nbgrsym  29561  upgrtrls  29897  upgristrl  29898  dfpth2  29926  usgr2pth0  29962  iswwlks  30033  isclwwlk  30183  clwwlkneq0  30228  h2hlm  31180  issh  31408  chcon2i  31664  chcon1i  31665  chcon3i  31666  chnlei  31685  cmcm2i  31793  cmcm3i  31794  3oalem3  31864  pjdifnormii  31883  pjneli  31923  dfadj2  32085  cnvadj  32092  hhcno  32104  hhcnf  32105  eleigvec  32157  eleigvec2  32158  pjimai  32376  isst  32413  ishst  32414  cvnbtwn4  32489  chrelat4i  32573  2reucom  32676  reuxfrdf  32687  difrab2  32694  inpr0  32728  iunin1f  32754  disjnf  32767  cbvdisjf  32768  disjorf  32776  iundisjf  32786  disjexc  32790  xrdifh  32979  iundisjfi  32995  hashxpe  33006  pmtrprfv2  33265  xrnarchi  33361  isunit2  33417  prmidl0  33634  opprnsg  33669  ccfldextdgrr  33966  cmpcref  34144  ordtconnlem1  34218  isrrext  34294  cntnevol  34522  ddemeas  34530  omssubaddlem  34593  omssubadd  34594  eulerpartleme  34657  eulerpartlemv  34658  eulerpartlemt0  34663  eulerpartlemgvv  34670  eulerpartlemn  34675  ballotlem2  34783  ballotlemodife  34792  oddprm2  34946  bnj257  35000  bnj268  35002  bnj290  35003  bnj312  35005  bnj89  35014  bnj887  35058  bnj976  35070  bnj1019  35072  bnj1146  35083  bnj1385  35124  bnj110  35150  bnj121  35162  bnj130  35166  bnj153  35172  bnj543  35185  bnj580  35205  bnj607  35208  bnj849  35217  bnj882  35218  bnj916  35225  bnj985v  35245  bnj985  35246  bnj1033  35261  bnj1083  35270  bnj1090  35271  bnj1128  35282  bnj1174  35295  bnj1228  35303  onvf1odlem1  35443  erdszelem1  35538  cvmliftlem15  35645  snmlval  35678  satfvsuclem2  35707  satfdm  35716  elmpst  35883  mpstrcl  35888  orbi2iALT  36032  untuni  36056  dfso3  36067  xpab  36073  dftr6  36098  coep  36099  coepr  36100  dffr5  36101  dfso2  36102  cnvco1  36106  cnvco2  36107  eldm3  36108  dfdm5  36120  dfrn5  36121  brsset  36234  idsset  36235  dfon3  36237  dfbigcup2  36244  dfom5b  36257  dffun10  36259  dfiota3  36268  fnimage  36274  brdomain  36278  brrange  36279  brimg  36282  brapply  36283  brcup  36284  brcap  36285  lemsuccf  36286  funpartlem  36289  brrestrict  36296  dfrecs2  36297  brub  36301  altopelaltxp  36323  rmoeqi  36544  rmoeqbii  36545  reueqi  36546  reueqbii  36547  sbceqbii  36548  disjeq1i  36549  cbvralvw2  36583  cbvrexvw2  36584  cbvrmovw2  36585  cbvreuvw2  36586  cbvsbcvw2  36587  cbvdisjvw2  36592  trer  36673  filnetlem4  36738  df3nandALT1  36756  imnand2  36759  mh-unprimbi  36901  bj-dfbi5  37014  bj-bixor  37031  bj-dfsbc  37121  bj-nnfnt  37222  bj-csbsnlem  37385  bj-rcleqf  37507  bj-sscon  37511  bj-pw0ALT  37531  bj-restpw  37579  bj-opelidb1  37642  bj-imdiridlem  37674  bj-imdirco  37679  wl-df3xor2  37960  wl-3xorrot  37968  wl-3xorcoma  37969  wl-3xornot  37972  wl-df2-3mintru2  37976  wl-df3-3mintru2  37977  wl-df4-3mintru2  37978  wl-equsalvw  38038  wl-sb9v  38049  iundif1  38090  poimirlem25  38141  poimirlem26  38142  poimirlem30  38146  ismblfin  38157  mbfposadd  38163  itg2addnclem2  38168  ftc1anc  38197  inixp  38224  prdstotbnd  38290  heibor1lem  38305  isrngohom  38461  isidl  38510  isfldidl2  38565  isdmn3  38570  sbccom2lem  38620  triantru3  38732  vvdifopab  38761  brres2  38769  eldmqsres  38789  inxpss  38813  ref5  38815  n0el2  38831  dfsucmap3  38959  trcoss2  39070  dfeqvrel2  39170  dfeqvrel3  39171  redundeq1  39209  redundpbi1  39211  refrelredund4  39215  funALTVfun  39279  dfeldisj3  39307  dfeldisj5  39309  pet0  39414  petid  39416  petidres  39418  petinidres  39420  petxrnidres  39422  mpet  39449  petincnvepres  39459  pet  39461  pmapglbx  40390  lhpexle3  40633  cdleme25cv  40979  dicelval3  41801  diclspsn  41815  lcfls1c  42157  sn-axrep5v  42833  sn-iotalem  42837  psspwb  42844  redvmptabs  42966  eu6w  43255  moxfr  43270  fphpd  43390  uniel  43791  dflim6  43838  onsucf1olem  43844  dflim7  43847  omge2  43872  oenassex  43892  safesnsupfilb  43991  ifpim1  44042  ifpnot  44043  ifpid2  44044  ifpim2  44045  ifpxorcor  44049  ifpnot23  44051  ifpananb  44079  ifpnannanb  44080  ifpxorxorb  44084  rp-fakeinunass  44088  snen1g  44097  pren2  44126  alephiso2  44131  undmrnresiss  44177  cnvssco  44179  cotrintab  44187  cnviun  44223  imaiun1  44224  coiun1  44225  elintima  44226  frege133d  44338  frege54cor0a  44436  or3or  44596  andi3or  44597  ntrneik4w  44673  k0004lem1  44720  ismnuprim  44867  ismnushort  44874  undisjrab  44879  nzss  44890  pm10.541  44940  compab  45014  onfrALTlem5  45115  onfrALTlem5VD  45457  rext0  45511  wfaxun  45572  brpermmodel  45576  permaxrep  45579  permaxpow  45582  permac8prim  45587  eluni2f  45678  euabsneu  47619  aiotaexb  47680  aiotavb  47681  r19.32  47689  3an4ancom24  47860  ichn  48059  ichcom  48062  ichbi12i  48063  prproropf1olem0  48105  pairreueq  48113  clnbgrsym  48457  usgrexmpl2nb0  48650  usgrexmpl2nb1  48651  usgrexmpl2nb2  48652  usgrexmpl2nb3  48653  usgrexmpl2nb4  48654  usgrexmpl2nb5  48655  sgrp2sgrp  48847  islindeps  49072  elbigo  49170  reutruALT  49423  coxp  49451  tposres0  49495  catcinv  50017  isthincd2  50055  setrec1lem3  50307  elpg  50332