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  2053  sb3an  2083  sbcom4  2091  sbbiiev  2094  excom  2164  sbal  2171  19.32  2235  19.31  2236  19.42  2238  equsalv  2269  sbex  2282  sbrim  2305  sbor  2307  sbbi  2308  sbnfOLD  2313  cbvex2v  2343  eeeanv  2349  sbnf2  2357  cbvsbvf  2362  cbvex2  2411  equsal  2416  dfsb3  2493  mo4  2560  eu6  2568  eubii  2579  dfeu  2589  sb8eulem  2592  sb8mo  2595  cbvmovw  2596  cbvmow  2597  cbveuvw  2599  cbveuw  2600  cbveuALT  2602  eu1  2604  sbmo  2608  cbvabv  2800  cbvabw  2801  cbvab  2802  eqabcb  2870  nfceqi  2889  ralbii2  3072  rexbii2  3073  r19.26-3  3091  r19.43  3098  r2allem  3118  r19.42v  3162  r19.32v  3163  reeanlem  3201  3reeanv  3203  cbvralvw  3208  cbvrexvw  3209  ralcom  3258  ralcomf  3268  rexcomf  3269  cbvralfw  3270  cbvralsvw  3281  cbvralf  3324  cbvrexf  3325  reu5  3346  rmobiia  3350  reubiia  3351  rmo5  3362  cbvrmovw  3365  cbvreuvw  3366  cbvrmow  3369  cbvreuw  3370  cbvreu  3385  cbvrmo  3386  rabid2f  3424  abv  3446  abvALT  3447  ceqsal  3472  ceqsalv  3474  cgsex4gOLD  3482  ceqsex3v  3490  ceqsex4v  3491  ceqsex8v  3493  reurab  3658  eueq  3665  reu2  3682  reu6  3683  reu3  3684  rmo4  3687  rmo3f  3691  2reu5  3715  cbvsbcw  3772  cbvsbcvw  3773  cbvsbc  3774  sbc3an  3804  sbccomlemOLD  3819  rmo3  3838  rmoanim  3843  rmoanimALT  3844  cbvralcsf  3890  cbvrexcsf  3891  cbvreucsf  3892  eqss  3948  uniiunlem  4035  sspsstri  4053  compleq  4100  ssequn1  4134  unss  4138  rexun  4144  ralunb  4145  elin3  4154  inass  4176  ssin  4187  elsymdif  4206  nssinpss  4215  dfun2  4218  difin  4220  indi  4232  indifdi  4242  difin2  4249  ssdif0  4314  inn0f  4319  inssdif0  4322  ab0  4328  abn0  4333  rabeq0w  4335  rabeq0  4336  disj  4398  disj3  4402  ssundif  4436  ralidmw  4456  dfif2  4475  eldifpr  4609  rexdifpr  4610  rexsns  4622  snprc  4668  reusn  4678  difsnpss  4757  tpss  4787  pwpr  4851  eluni2  4861  elunirab  4872  uniun  4880  unissb  4889  elintrab  4908  ssintrab  4919  intun  4928  iuncom  4947  iuncom4  4948  iunab  4998  ssiinf  5001  iunn0  5013  iinab  5014  iunin2  5017  iinun2  5019  iundif2  5020  iunun  5039  iunxun  5040  iunxiun  5043  sspwuni  5046  iinpw  5052  cbvdisj  5066  cbvdisjv  5067  disjor  5071  brun  5140  brin  5141  brdif  5142  dftr2  5198  dftr5  5200  intexrab  5283  inuni  5286  ssext  5393  pweqb  5395  otth2  5421  otthne  5424  propeqop  5445  vopelopabsb  5467  eqopab2bw  5486  eqopab2b  5490  pwin  5505  pwun  5507  dffr6  5570  elxp2  5638  otelxp  5658  xpiundi  5685  xpiundir  5686  poinxp  5695  soinxp  5696  frinxp  5697  seinxp  5698  weinxp  5699  inopab  5767  difopab  5768  inxp  5769  raliunxp  5777  rexiunxp  5778  rexxpf  5785  iunxpf  5786  cnvco  5823  dmiun  5851  dmuni  5852  dm0rn0  5862  dmres  5958  restidsing  5999  asymref  6060  codir  6064  qfto  6065  cnvopab  6081  cnvopabOLD  6082  cnvdif  6087  rniun  6091  dminss  6097  imainss  6098  difxp  6108  xpdifid  6112  dmsnn0  6151  cnvcnvsn  6163  cnvresima  6174  resco  6194  imaco  6195  rnco  6196  coiun  6200  coass  6209  ressn  6228  cnviin  6229  cnvpo  6230  cnvso  6231  xpco  6232  opreu2reurex  6237  dfpo2  6239  imaindm  6242  dflim2  6360  funcnv  6546  funcnv3  6547  fncnv  6550  fun11  6551  imadif  6561  fnres  6604  dfmpt3  6611  mptfnf  6612  fnopabg  6614  fint  6698  fin  6699  fores  6741  dff1o3  6765  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  9755  cp  9776  isinfcard  9975  aceq1  10000  aceq2  10002  dfac5lem3  10008  dfac10b  10023  dfac12a  10032  dffin7-2  10281  dfacfin7  10282  fin1a2lem6  10288  iunfo  10422  konigthlem  10451  axgroth6  10711  axgroth3  10714  sstskm  10725  ltexprlem1  10919  gt0srpr  10961  ltpsrpr  10992  map2psrpr  10993  ltresr  11023  fimaxre3  12060  sup3  12071  supaddc  12081  supmul1  12083  elnn0z  12473  elznn0nn  12474  zmin  12834  xrnemnf  13008  xrnepnf  13009  dfrp2  13286  elioomnf  13336  elxrge0  13349  elfzuzb  13410  fzass4  13454  elfz2nn0  13510  elfzo2  13554  elfzo3  13568  lbfzo0  13591  fzo1lb  13605  fzind2  13680  nn0opthlem1  14167  hashgt23el  14323  cotr2g  14875  rexfiuz  15247  fsumcom2  15673  prodmo  15835  fprodcom2  15883  sinltx  16090  divalglem4  16299  divalglem10  16305  4sqlem12  16860  imasleval  17437  xpsfrnel  17458  xpscf  17461  isssc  17719  isffth2  17817  ispos2  18213  issubmgm  18602  ismhm  18685  issubmndb  18705  nsgacs  19067  isgim  19167  oppgcntz  19269  f1omvdco3  19354  pmtrprfvalrn  19393  efgrelexlemb  19655  pgpfac1  19987  pgpfac  19991  issrg  20099  opprsubg  20263  opprunit  20288  isirred2  20332  opprirred  20333  opprnzrb  20429  isdomn2OLD  20620  opprdomnb  20625  isdomn4r  20627  drngprop  20652  opprdrng  20672  issdrg2  20703  isorng  20769  islss  20860  islbs  21003  unocv  21610  iunocv  21611  isbasis2g  22856  tgval2  22864  ntreq0  22985  isclo2  22996  cmpcov2  23298  is1stc2  23350  1stcelcls  23369  llyi  23382  unisngl  23435  txuni2  23473  xkobval  23494  hausdiag  23553  isfbas2  23743  elfg  23779  fbasrn  23792  fmfnfmlem3  23864  isfcls  23917  alexsubALTlem2  23956  istmd  23982  istgp  23985  istrg  24072  istdrg  24074  istdrg2  24086  isms2  24358  metuel2  24473  restmetu  24478  isngp  24504  isngp2  24505  isngp3  24506  elii1  24851  isncvsngp  25069  iscph  25090  isbn  25258  pmltpc  25371  ovolfcl  25387  finiunmbl  25465  iundisj  25469  dyaddisj  25517  vitalilem1  25529  ellimc3  25800  ig1pval3  26103  plyun0  26122  plydivex  26225  aannenlem2  26257  ellogrn  26488  atandm  26806  atandm3  26808  atans2  26861  elno3  27587  conway  27733  eqscut2  27740  madeval2  27787  tgjustf  28444  colinearalg  28881  axeuclid  28934  nbgrsym  29334  upgrtrls  29671  upgristrl  29672  dfpth2  29700  usgr2pth0  29736  iswwlks  29807  isclwwlk  29954  clwwlkneq0  29999  h2hlm  30950  issh  31178  chcon2i  31434  chcon1i  31435  chcon3i  31436  chnlei  31455  cmcm2i  31563  cmcm3i  31564  3oalem3  31634  pjdifnormii  31653  pjneli  31693  dfadj2  31855  cnvadj  31862  hhcno  31874  hhcnf  31875  eleigvec  31927  eleigvec2  31928  pjimai  32146  isst  32183  ishst  32184  cvnbtwn4  32259  chrelat4i  32343  2reucom  32449  reuxfrdf  32460  difrab2  32467  inpr0  32502  iunin1f  32527  disjnf  32540  cbvdisjf  32541  disjorf  32549  iundisjf  32559  disjexc  32563  xrdifh  32753  iundisjfi  32768  hashxpe  32779  pmtrprfv2  33047  xrnarchi  33143  isunit2  33197  prmidl0  33405  opprnsg  33439  ccfldextdgrr  33675  cmpcref  33853  ordtconnlem1  33927  isrrext  34003  cntnevol  34231  ddemeas  34239  omssubaddlem  34302  omssubadd  34303  eulerpartleme  34366  eulerpartlemv  34367  eulerpartlemt0  34372  eulerpartlemgvv  34379  eulerpartlemn  34384  ballotlem2  34492  ballotlemodife  34501  oddprm2  34658  bnj257  34709  bnj268  34711  bnj290  34712  bnj312  34714  bnj89  34723  bnj887  34767  bnj976  34779  bnj1019  34781  bnj1146  34793  bnj1385  34834  bnj110  34860  bnj121  34872  bnj130  34876  bnj153  34882  bnj543  34895  bnj580  34915  bnj607  34918  bnj849  34927  bnj882  34928  bnj916  34935  bnj985v  34955  bnj985  34956  bnj1033  34971  bnj1083  34980  bnj1090  34981  bnj1128  34992  bnj1174  35005  bnj1228  35013  onvf1odlem1  35115  erdszelem1  35203  cvmliftlem15  35310  snmlval  35343  satfvsuclem2  35372  satfdm  35381  elmpst  35548  mpstrcl  35553  orbi2iALT  35697  untuni  35721  dfso3  35732  xpab  35738  dftr6  35763  coep  35764  coepr  35765  dffr5  35766  dfso2  35767  cnvco1  35771  cnvco2  35772  eldm3  35773  dfdm5  35785  dfrn5  35786  brsset  35902  idsset  35903  dfon3  35905  dfbigcup2  35912  dfom5b  35925  dffun10  35927  dfiota3  35936  fnimage  35942  brdomain  35946  brrange  35947  brimg  35950  brapply  35951  brcup  35952  brcap  35953  brsuccf  35954  funpartlem  35955  brrestrict  35962  dfrecs2  35963  brub  35967  altopelaltxp  35989  rmoeqi  36200  rmoeqbii  36201  reueqi  36202  reueqbii  36203  sbceqbii  36204  disjeq1i  36205  cbvralvw2  36239  cbvrexvw2  36240  cbvrmovw2  36241  cbvreuvw2  36242  cbvsbcvw2  36243  cbvdisjvw2  36248  trer  36329  filnetlem4  36394  df3nandALT1  36412  imnand2  36415  bj-dfbi5  36587  bj-bixor  36604  bj-nnfnt  36753  bj-csbsnlem  36916  bj-rcleqf  37038  bj-sscon  37042  bj-pw0ALT  37062  bj-restpw  37105  bj-opelidb1  37166  bj-imdiridlem  37198  bj-imdirco  37203  wl-df3xor2  37482  wl-3xorrot  37490  wl-3xorcoma  37491  wl-3xornot  37494  wl-df2-3mintru2  37498  wl-df3-3mintru2  37499  wl-df4-3mintru2  37500  wl-equsalvw  37551  wl-sb9v  37562  iundif1  37613  poimirlem25  37664  poimirlem26  37665  poimirlem30  37669  ismblfin  37680  mbfposadd  37686  itg2addnclem2  37691  ftc1anc  37720  inixp  37747  prdstotbnd  37813  heibor1lem  37828  isrngohom  37984  isidl  38033  isfldidl2  38088  isdmn3  38093  sbccom2lem  38143  triantru3  38243  vvdifopab  38274  brres2  38282  eldmqsres  38300  inxpss  38324  ref5  38326  n0el2  38342  trcoss2  38500  dfeqvrel2  38606  dfeqvrel3  38607  redundeq1  38645  redundpbi1  38647  refrelredund4  38651  funALTVfun  38715  dfeldisj3  38736  dfeldisj5  38738  pet0  38832  petid  38834  petidres  38836  petinidres  38838  petxrnidres  38840  mpet  38856  petincnvepres  38866  pet  38868  pmapglbx  39787  lhpexle3  40030  cdleme25cv  40376  dicelval3  41198  diclspsn  41212  lcfls1c  41554  sn-axrep5v  42228  sn-iotalem  42233  psspwb  42240  redvmptabs  42372  eu6w  42688  moxfr  42704  fphpd  42828  uniel  43229  dflim6  43276  onsucf1olem  43282  dflim7  43285  omge2  43310  oenassex  43330  safesnsupfilb  43430  ifpim1  43481  ifpnot  43482  ifpid2  43483  ifpim2  43484  ifpxorcor  43488  ifpnot23  43490  ifpananb  43518  ifpnannanb  43519  ifpxorxorb  43523  rp-fakeinunass  43527  snen1g  43536  pren2  43565  alephiso2  43570  undmrnresiss  43616  cnvssco  43618  cotrintab  43626  cnviun  43662  imaiun1  43663  coiun1  43664  elintima  43665  frege133d  43777  frege54cor0a  43875  or3or  44035  andi3or  44036  ntrneik4w  44112  k0004lem1  44159  ismnuprim  44306  ismnushort  44313  undisjrab  44318  nzss  44329  pm10.541  44379  compab  44453  onfrALTlem5  44554  onfrALTlem5VD  44896  rext0  44950  wfaxun  45011  brpermmodel  45015  permaxrep  45018  permaxpow  45021  permac8prim  45026  eluni2f  45119  euabsneu  47038  aiotaexb  47099  aiotavb  47100  r19.32  47108  3an4ancom24  47279  ichn  47466  ichcom  47469  ichbi12i  47470  prproropf1olem0  47512  pairreueq  47520  clnbgrsym  47848  usgrexmpl2nb0  48041  usgrexmpl2nb1  48042  usgrexmpl2nb2  48043  usgrexmpl2nb3  48044  usgrexmpl2nb4  48045  usgrexmpl2nb5  48046  sgrp2sgrp  48238  islindeps  48464  elbigo  48562  reutruALT  48815  coxp  48843  tposres0  48887  catcinv  49410  isthincd2  49448  setrec1lem3  49700  elpg  49725