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 ⊢ (𝜒 ↔ 𝜃)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  bibi2d  346  pm4.71  561  pm5.32ri  579  an31  647  pm4.14  806  or4  924  orimdi  928  orbidi  950  ordi  1003  ordir  1004  andir  1006  dfbi3  1045  dfifp7  1065  ifpdfbi  1066  ifpn  1069  ifpnOLD  1070  3orrot  1089  3orcoma  1090  3ioran  1103  3ianor  1104  3anbi123i  1152  3orbi123i  1153  an6  1442  3or6  1444  an33rean  1480  an33reanOLD  1481  nancom  1487  xorcomOLD  1506  xorass  1507  xorbi12iOLD  1517  anxordi  1519  norcomOLD  1524  nornotOLD  1526  norass  1534  hadbi  1599  hadcoma  1600  hadcomaOLD  1601  hadcomb  1602  hadnot  1604  cador  1610  cadan  1611  cadcoma  1614  cadnot  1617  nic-axALT  1676  nfnbi  1856  19.26-3an  1873  19.43OLD  1884  19.32v  1941  19.31v  1942  19.42v  1954  4exdistr  1963  cbvexvw  2044  sbcom4  2096  sbcom3vv  2103  sbal  2163  excom  2166  19.32  2233  19.31  2234  19.42  2236  equsalv  2265  sbex  2284  sbanOLD  2308  sbor  2312  sbbi  2313  sbanvOLD  2319  sbbivOLD  2320  cbvexv1  2351  cbvex2v  2354  eeeanv  2360  sbnf2  2366  cbvex2  2423  equsal  2428  dfsb3  2512  dfsb3ALT  2568  sbanALT  2586  sbbiALT  2587  mo4  2625  eu6  2634  eubii  2645  dfeu  2656  sb8eulem  2659  sb8mo  2662  cbvmow  2663  cbvmowOLD  2664  cbveuw  2666  cbveuALT  2669  eu1  2671  sbmo  2675  cbvabv  2866  cbvabw  2867  cbvabwOLD  2868  cbvab  2869  abeq1  2923  nfceqi  2952  sbabel  2986  ralbii2  3131  r19.21v  3142  r2allem  3165  ralcom4  3198  rexbii2  3208  reuanid  3286  rmoanid  3287  r19.32v  3294  r19.41v  3300  r19.41  3301  r19.42v  3303  r19.43  3304  ralcom  3307  rexcomOLD  3309  ralcomf  3310  rexcomf  3311  reeanlem  3318  3reeanv  3321  2ralor  3322  rabid2  3334  rabid2f  3335  rabbi  3336  reubiia  3343  rmobiia  3348  reu5  3375  rmo5  3379  cbvralfw  3382  cbvralfwOLD  3383  cbvrexfw  3384  cbvralf  3385  cbvrexf  3386  cbvreuw  3389  cbvrmow  3390  cbvrmowOLD  3391  cbvreu  3394  cbvrmo  3395  cbvralvw  3396  cbvrexvw  3397  vjust  3442  abv  3451  cgsex4g  3486  ceqsex3v  3493  ceqsex4v  3494  ceqsex8v  3496  eueq  3647  reu2  3664  reu6  3665  reu3  3666  rmo4  3669  rmo3f  3673  2reu5  3697  cbvsbcw  3752  cbvsbc  3754  sbccomlem  3799  rmo3  3818  rmoanim  3823  rmoanimALT  3824  cbvralcsf  3870  cbvrexcsf  3871  cbvreucsf  3872  dfss2  3901  eqss  3930  uniiunlem  4012  sspsstri  4030  compleq  4075  ssequn1  4107  unss  4111  rexun  4117  ralunb  4118  elin3  4127  incomOLD  4129  inass  4146  ssin  4157  elsymdif  4174  nssinpss  4183  dfun2  4186  difin  4188  indi  4200  indifdir  4210  ssdif0  4277  inssdif0  4283  rabeq0  4292  disj  4355  disj3  4361  ssundif  4391  dfif2  4427  eldifpr  4557  rexsns  4569  snprc  4613  reusn  4623  difsnpss  4700  tpss  4728  pwpr  4794  eluni2  4804  elunirab  4816  uniun  4823  unissb  4832  elintrab  4850  ssintrab  4861  intun  4870  intpr  4871  iuncom  4888  iuncom4  4889  iunab  4938  ssiinf  4941  iunn0  4952  iinab  4953  iunin2  4956  iinun2  4958  iundif2  4959  iunun  4978  iunxun  4979  iunxiun  4982  sspwuni  4985  iinpw  4991  cbvdisj  5005  disjor  5010  brun  5081  brin  5082  brdif  5083  dftr2  5138  intexrab  5207  inuni  5210  ssext  5312  pweqb  5314  otth2  5340  propeqop  5362  opelopabsbALT  5381  eqopab2bw  5400  eqopab2b  5404  pwin  5419  pwun  5423  elxp2  5543  xpiundi  5586  xpiundir  5587  poinxp  5596  soinxp  5597  frinxp  5598  seinxp  5599  weinxp  5600  inopab  5665  difopab  5666  raliunxp  5674  rexiunxp  5675  rexxpf  5682  iunxpf  5683  cnvco  5720  dmiun  5746  dmuni  5747  dm0rn0  5759  dmres  5840  restidsing  5889  cnvsym  5941  asymref  5943  codir  5947  qfto  5948  cnvopab  5964  cnvdif  5969  rniun  5973  dminss  5977  imainss  5978  difxp  5988  xpdifid  5992  dmsnn0  6031  cnvcnvsn  6043  cnvresima  6054  resco  6070  imaco  6071  rnco  6072  coiun  6076  coass  6085  ressn  6104  cnviin  6105  cnvpo  6106  cnvso  6107  xpco  6108  opreu2reurex  6113  dflim2  6215  unisuc  6235  funcnv  6393  funcnv3  6394  fncnv  6397  fun11  6398  imadif  6408  fnres  6446  dfmpt3  6454  mptfnf  6455  fnopabg  6457  fint  6532  fin  6533  fores  6575  dff1o3  6596  f1ompt  6852  fsn  6874  imaiun  6982  isocnv2  7063  isocnv3  7064  isores2  7065  isomin  7069  eqoprab2bw  7203  eqoprab2b  7204  elpwpwel  7469  sucexb  7504  sucelon  7512  dflim4  7543  fiun  7626  f1iun  7627  f11o  7630  opabex3d  7648  opabex3rd  7649  opabex3  7650  dfopab2  7732  dfoprab3s  7733  fmpox  7747  fparlem1  7790  fparlem2  7791  fsplitOLD  7796  suppvalbr  7817  tpostpos  7895  wfrlem8  7945  wfrfun  7948  dfsmo2  7967  brwitnlem  8115  oarec  8171  qsid  8346  uniinqs  8360  mapval2  8419  mapsncnv  8440  elixp2  8448  ixpin  8470  brsdom  8515  brdom2  8522  xpassen  8594  brsdom2  8625  unfilem1  8766  fiint  8779  dfsup2  8892  supmo  8900  eqinf  8932  infmo  8943  rankc1  9283  cp  9304  isinfcard  9503  aceq1  9528  aceq2  9530  dfac5lem3  9536  dfac10b  9550  dfac12a  9559  dffin7-2  9809  dfacfin7  9810  fin1a2lem6  9816  iunfo  9950  konigthlem  9979  axgroth6  10239  axgroth3  10242  sstskm  10253  ltexprlem1  10447  gt0srpr  10489  ltpsrpr  10520  map2psrpr  10521  ltresr  10551  fimaxre3  11575  sup3  11585  supaddc  11595  supmul1  11597  elnn0z  11982  elznn0nn  11983  zmin  12332  xrnemnf  12500  xrnepnf  12501  elioomnf  12822  elxrge0  12835  elfzuzb  12896  fzass4  12940  elfz2nn0  12993  elfzo2  13036  elfzo3  13049  lbfzo0  13072  fzind2  13150  nn0opthlem1  13624  hashgt23el  13781  cotr2g  14327  rexfiuz  14699  fsumcom2  15121  prodmo  15282  fprodcom2  15330  sinltx  15534  divalglem4  15737  divalglem10  15743  4sqlem12  16282  imasleval  16806  xpsfrnel  16827  xpscf  16830  isssc  17082  isffth2  17178  ispos2  17550  ismhm  17950  issubmndb  17962  nsgacs  18306  isgim  18394  oppgcntz  18484  f1omvdco3  18569  pmtrprfvalrn  18608  efgrelexlemb  18868  pgpfac1  19195  pgpfac  19199  issrg  19250  opprsubg  19382  opprunit  19407  isirred2  19447  opprirred  19448  drngprop  19506  opprdrng  19519  issdrg2  19570  islss  19699  islbs  19841  isdomn2  20065  unocv  20369  iunocv  20370  isbasis2g  21553  tgval2  21561  ntreq0  21682  isclo2  21693  cmpcov2  21995  is1stc2  22047  1stcelcls  22066  llyi  22079  unisngl  22132  txuni2  22170  xkobval  22191  hausdiag  22250  isfbas2  22440  elfg  22476  fbasrn  22489  fmfnfmlem3  22561  isfcls  22614  alexsubALTlem2  22653  istmd  22679  istgp  22682  istrg  22769  istdrg  22771  istdrg2  22783  isms2  23057  metuel2  23172  restmetu  23177  isngp  23202  isngp2  23203  isngp3  23204  elii1  23540  isncvsngp  23754  iscph  23775  isbn  23942  pmltpc  24054  ovolfcl  24070  finiunmbl  24148  iundisj  24152  dyaddisj  24200  vitalilem1  24212  ellimc3  24482  ig1pval3  24775  plyun0  24794  plydivex  24893  aannenlem2  24925  ellogrn  25151  atandm  25462  atandm3  25464  atans2  25517  tgjustf  26267  colinearalg  26704  axeuclid  26757  nbgrsym  27153  upgrtrls  27491  upgristrl  27492  usgr2pth0  27554  iswwlks  27622  isclwwlk  27769  clwwlkneq0  27814  h2hlm  28763  issh  28991  chcon2i  29247  chcon1i  29248  chcon3i  29249  chnlei  29268  cmcm2i  29376  cmcm3i  29377  3oalem3  29447  pjdifnormii  29466  pjneli  29506  dfadj2  29668  cnvadj  29675  hhcno  29687  hhcnf  29688  eleigvec  29740  eleigvec2  29741  pjimai  29959  isst  29996  ishst  29997  cvnbtwn4  30072  chrelat4i  30156  2reucom  30250  moel  30259  reuxfrdf  30262  difrab2  30268  inpr0  30304  iunin1f  30321  disjnf  30333  cbvdisjf  30334  disjorf  30342  iundisjf  30352  disjexc  30356  dfrp2  30517  xrdifh  30529  iundisjfi  30545  hashxpe  30555  pmtrprfv2  30782  xrnarchi  30863  isorng  30923  prmidl0  31034  ccfldextdgrr  31145  cmpcref  31203  ordtconnlem1  31277  isrrext  31351  cntnevol  31597  ddemeas  31605  omssubaddlem  31667  omssubadd  31668  eulerpartleme  31731  eulerpartlemv  31732  eulerpartlemt0  31737  eulerpartlemgvv  31744  eulerpartlemn  31749  ballotlem2  31856  ballotlemodife  31865  oddprm2  32036  bnj257  32087  bnj268  32089  bnj290  32090  bnj312  32092  bnj89  32101  bnj887  32146  bnj976  32159  bnj1019  32161  bnj1146  32173  bnj1385  32214  bnj110  32240  bnj121  32252  bnj130  32256  bnj153  32262  bnj543  32275  bnj580  32295  bnj607  32298  bnj849  32307  bnj882  32308  bnj916  32315  bnj985v  32335  bnj985  32336  bnj1033  32351  bnj1083  32360  bnj1090  32361  bnj1128  32372  bnj1174  32385  bnj1228  32393  erdszelem1  32551  cvmliftlem15  32658  snmlval  32691  satfvsuclem2  32720  satfdm  32729  elmpst  32896  mpstrcl  32901  untuni  33048  dfso3  33063  dftr6  33099  coep  33100  coepr  33101  dffr5  33102  dfso2  33103  dfpo2  33104  cnvco1  33108  cnvco2  33109  eldm3  33110  dfdm5  33129  dfrn5  33130  imaindm  33135  frrlem9  33244  elno3  33275  conway  33377  madeval2  33403  brsset  33463  idsset  33464  dfon3  33466  dfbigcup2  33473  dfom5b  33486  dffun10  33488  dfiota3  33497  fnimage  33503  brdomain  33507  brrange  33508  brimg  33511  brapply  33512  brcup  33513  brcap  33514  brsuccf  33515  funpartlem  33516  brrestrict  33523  dfrecs2  33524  brub  33528  altopelaltxp  33550  trer  33777  filnetlem4  33842  df3nandALT1  33860  imnand2  33863  bj-dfbi5  34020  bj-bixor  34038  bj-nnfnt  34184  bj-sbnf  34279  bj-csbsnlem  34344  bj-rcleqf  34461  bj-sscon  34465  bj-pw0ALT  34466  bj-restpw  34507  bj-opelidb1  34568  bj-imdiridlem  34600  bj-imdirco  34605  wl-df3xor2  34886  wl-3xorrot  34894  wl-3xorcoma  34895  wl-3xornot  34898  wl-df2-3mintru2  34902  wl-df3-3mintru2  34903  wl-df4-3mintru2  34904  wl-equsalvw  34943  wl-dfrexv  35014  wl-dfrexex  35015  wl-dfrmosb  35018  wl-dfrmov  35019  wl-dfreusb  35022  wl-dfreuv  35023  wl-dfrabv  35027  iundif1  35031  poimirlem25  35082  poimirlem26  35083  poimirlem30  35087  ismblfin  35098  mbfposadd  35104  itg2addnclem2  35109  ftc1anc  35138  inixp  35166  prdstotbnd  35232  heibor1lem  35247  isrngohom  35403  isidl  35452  isfldidl2  35507  isdmn3  35512  sbccom2lem  35562  triantru3  35660  vvdifopab  35681  brres2  35689  eldmqsres  35703  inxpss  35729  n0el2  35750  trcoss2  35884  dfeqvrel2  35985  dfeqvrel3  35986  redundeq1  36024  redundpbi1  36026  refrelredund4  36030  funALTVfun  36091  dfeldisj3  36112  dfeldisj5  36114  pmapglbx  37065  lhpexle3  37308  cdleme25cv  37654  dicelval3  38476  diclspsn  38490  lcfls1c  38832  sn-axrep5v  39400  psspwb  39408  moxfr  39633  fphpd  39757  ifpim1  40177  ifpnot  40178  ifpid2  40179  ifpim2  40180  ifpxorcor  40184  ifpnot23  40186  ifpananb  40214  ifpnannanb  40215  ifpxorxorb  40219  rp-fakeinunass  40223  snen1g  40232  pren2  40252  alephiso2  40257  undmrnresiss  40304  cnvssco  40306  cotrintab  40314  cnviun  40351  imaiun1  40352  coiun1  40353  elintima  40354  frege133d  40466  frege54cor0a  40564  or3or  40724  andi3or  40725  ntrneik4w  40803  k0004lem1  40850  ismnuprim  41002  undisjrab  41010  nzss  41021  pm10.541  41071  compab  41146  onfrALTlem5  41248  onfrALTlem5VD  41591  inn0f  41707  eluni2f  41739  euabsneu  43620  aiotaexb  43646  aiotavb  43647  r19.32  43653  3an4ancom24  43825  ichn  43973  ichcom  43976  ichbi12i  43977  prproropf1olem0  44019  pairreueq  44027  issubmgm  44409  sgrp2sgrp  44488  islindeps  44862  elbigo  44965  setrec1lem3  45219  elpg  45243