Theorem 3bitri 300

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
3bitri.1	⊢ (𝜑 ↔ 𝜓)
3bitri.2	⊢ (𝜓 ↔ 𝜒)
3bitri.3	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
3bitri	⊢ (𝜑 ↔ 𝜃)

Proof of Theorem 3bitri

Step	Hyp	Ref	Expression
1		3bitri.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		3bitri.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3		3bitri.3	. . 3 ⊢ (𝜒 ↔ 𝜃)
4	2, 3	bitri 278	. 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:  bibi1i  341  pm5.32  583  biadan  830  orbi1i  926  orass  934  or32  938  cases  1056  dn1  1071  3anidm  1119  an33rean  1507  nanbi  1523  excxor  1539  cadan  1632  cadcomb  1636  nic-axALT  1697  tbw-bijust  1721  rb-bijust  1772  nf2  1808  19.43  1905  19.43OLD  1906  3exdistr  1983  19.12vvv  2017  sbco4  2139  excom13  2201  sbcom2  2209  sbco4OLD  2211  sbn  2317  sbnf  2348  19.12vv  2381  eeeanv  2384  ee4anv  2385  ee4anvOLD  2386  2sb8ef  2390  sbel2x  2508  2sb8e  2564  dfmo2  2626  sb8eulem  2628  2mo2  2677  2eu7  2687  2eu8  2688  sbabel  2959  3r19.43  3134  r19.23v  3192  2ralor  3239  rexcom13  3298  cbvreu  3409  rabrabi  3436  cgsex4g  3503  ceqsex2  3507  ceqsex2v  3508  ceqsex3v  3509  ceqsex4v  3510  ceqsex6v  3511  ceqsex8v  3512  ralrab2  3664  rexrab2  3666  reu2  3691  rmo4  3696  reu8  3699  rmo3f  3700  2reu5lem3  3723  sbcimdv  3815  reu8nf  3833  rmo2  3843  rmo3  3845  rmoanim  3850  ss2rab  4025  rabss  4026  ssrab  4027  dfdif3OLD  4075  symdifass  4217  dfss4  4224  undi  4240  indifdi  4249  undif3  4255  reuun2  4280  difin0ss  4329  disj  4407  disj4  4416  rabsssn  4630  disjsn  4673  snssb  4744  raldifsni  4758  ssunpr  4794  sspr  4795  sstp  4796  uni0b  4894  uni0c  4895  ssint  4924  intprg  4941  iunssf  5002  iunssfOLD  5003  iunss  5004  iunssOLD  5005  iundif2  5033  disjor  5086  nfnid  5336  reusv2lem4  5362  ssextss  5424  exss  5434  eqvinop  5459  sbcop  5461  opcom  5474  opeqpr  5478  brtp  5497  brabsb  5505  opelopabf  5520  dfid3  5549  pofun  5577  opeliunxp  5718  opeliun2xp  5719  xpiundi  5722  brinxp2  5729  exopxfr  5819  cnvuni  5866  dmopab3  5899  rnep  5907  dmxp  5909  rnopab3  5936  elres  6009  elsnres  6010  elrid  6038  cnvsym  6104  asymref2  6107  intirr  6108  cnvopab  6127  xpeq0  6148  difxp  6152  xpdifid  6156  xpdifcnvepel  6157  ssrnres  6167  dminxp  6169  dfrel4v  6179  elid  6189  dmsnn0  6197  imaco  6241  rnco  6242  rncoOLD  6243  coeq0  6246  resssxp  6260  dfpo2  6286  snres0  6288  sspred  6300  frpoind  6332  sb8iota  6492  fun11  6599  isarep1  6614  dff1o4  6819  opabiota  6953  fvopab5  7013  eqfnfv3  7017  fvn0ssdmfun  7059  fnressn  7145  f13dfv  7262  dff1o6  7263  fliftel  7297  oprabidw  7431  oprabid  7432  eloprabga  7509  mpo2eqb  7532  ralrnmpo  7539  uniuni  7749  dflim3  7831  dfom2  7852  elxp4  7907  elxp5  7908  opabex3d  7950  opabex3rd  7951  opabex3  7952  el2xptp  8020  fsplit  8100  xporderlem  8111  ralxp3f  8121  frpoins3xpg  8124  poxp2  8127  suppvalbr  8148  dfrecs3  8347  tz7.48lem  8416  seqomlem2  8426  oaord  8520  oeeu  8577  nnaord  8593  ecid  8766  mptelixpg  8921  elixpsn  8923  xpsnen  9037  xpcomco  9043  xpassen  9047  omxpenlem  9054  modom  9199  brttrcl2  9671  ttrcltr  9673  rnttrcl  9679  frind  9710  tz9.12lem3  9749  rankxpsuc  9842  cp  9865  cardprclem  9953  infxpenlem  9985  dfac5lem1  10095  dfac5lem2  10096  dfac5lem5  10099  dfac10c  10110  kmlem3  10124  kmlem12  10133  kmlem13  10134  kmlem14  10135  kmlem15  10136  ackbij2  10213  cf0  10222  cflim2  10235  dffin7-2  10370  dfacfin7  10371  fin1a2lem12  10383  axdc3lem3  10424  cfpwsdom  10557  recmulnq  10937  genpass  10982  psslinpr  11004  suplem2pr  11026  opelreal  11103  ltxrlt  11268  addrid  11378  ind1a  12217  elnn0  12494  elxnn0  12567  elnn0z  12592  nnwos  12927  elxr  13129  xrnepnf  13131  elfzuzb  13534  4fvwrd4  13664  preduz  13666  elfzo2  13678  ssnn0fi  14009  sqeqori  14238  xpcogend  14999  cotr2g  15001  fsumcom2  15813  modfsummod  15834  fprodcom2  16026  rpnnen2lem12  16269  gcdcllem1  16545  isprm2  16728  isprm7  16755  pythagtriplem2  16865  infpn2  16961  4sqlem12  17004  initoid  18046  termoid  18047  eldmcoa  18110  oduposb  18371  gsumwspan  18893  smndex1basss  18955  smndex1mgm  18957  isnsg2  19210  isnsg4  19221  cycsubmel  19259  efgcpbllemb  19813  dmdprd  20058  dprdval  20063  dprdw  20070  dprd2d2  20104  dfrhm2  20544  brric2  20577  issubrg  20644  isdomn5  20783  islmim  21149  lbsextlem2  21249  prmidl0  21435  cnfldfun  21493  pzriprnglem3  21590  pjfval2  21816  opsrtoslem1  22163  ntreq0  23191  cmpcov2  23504  cmpsub  23514  2ndcdisj  23570  unisngl  23641  txbas  23681  elpt  23686  txkgen  23766  xkococn  23774  fbun  23954  trfil2  24001  fin1aufil  24046  alexsubALTlem3  24163  cnextcn  24181  qustgplem  24235  eltsms  24247  ustn0  24335  fmucndlem  24404  metrest  24638  restmetu  24684  isclmp  25213  srabn  25476  ellogdm  26758  1cubr  26961  leibpilem2  27060  dmarea  27076  vmasum  27334  dchrelbas2  27355  2lgslem4  27524  nosupbnd1lem4  27829  nosupbnd2lem1  27833  lenlts  27870  madeval2  27980  made0  28010  oniso  28418  onsfi  28503  tgcgr4  28754  ltgov  28820  plngrotlem2  29014  axlowdimlem13  29209  axeuclidlem  29217  numedglnl  29399  nbupgrres  29619  vtxd0nedgb  29743  rusgrprc  29845  usgr2pth0  30019  wspthsnwspthsnon  30170  isclwwlk  30240  clwwlkn1  30297  clwwlkn2  30300  clwwlknonel  30351  3pthdlem1  30420  iseupthf1o  30458  frgr3v  30531  fusgr2wsp2nb  30590  frgrregord013  30651  h2hcau  31236  h2hlm  31237  shlesb1i  31643  shne0i  31705  chnlei  31742  cmbr2i  31853  pjneli  31980  ho02i  32086  adjsym  32090  adjeu  32146  lnopeqi  32265  largei  32524  atoml2i  32640  cdj3lem3b  32697  or3di  32712  mo5f  32741  dmrab  32749  rabsspr  32753  rabsstp  32754  disjnf  32821  disjorf  32830  ssrelf  32868  ofpreima  32918  disjdsct  32956  1stpreima  32960  2ndpreima  32961  f1od2  32972  xrdifh  33033  nndiffz1  33039  domnprodeq0  33507  zarclsun  34172  ordtconnlem1  34226  measiuns  34519  elunirnmbfm  34554  eulerpartlemr  34676  eulerpartlemgh  34680  eulerpartlemn  34683  ballotlemodife  34800  bnj250  35002  bnj334  35014  bnj345  35015  bnj89  35022  bnj115  35026  bnj919  35068  bnj1304  35119  bnj92  35162  bnj124  35171  bnj126  35173  bnj154  35178  bnj155  35179  bnj523  35187  bnj526  35188  bnj540  35192  bnj581  35208  bnj916  35233  bnj929  35236  bnj964  35243  bnj978  35249  bnj983  35251  bnj1039  35271  bnj1040  35272  bnj1123  35286  bnj1128  35290  bnj1398  35334  lfuhgr3  35478  cvmlift2lem1  35660  satfv0  35716  satf0  35730  satf0op  35735  satffunlem  35759  satffunlem1lem1  35760  satffunlem2lem1  35762  elmthm  35934  quad3  36028  3orit  36074  dftr6  36109  eldm3  36119  elrn3  36120  elima4  36134  19.12b  36157  brtxp  36236  brtxp2  36237  brpprod  36241  brpprod3a  36242  elfix  36259  dffix2  36261  ellimits  36266  sscoid  36269  dffun10  36270  elfuns  36271  elsingles  36274  brimg  36293  brapply  36294  lemsuccf  36297  brsuccf  36298  funpartlem  36300  brrestrict  36307  dfrecs2  36308  dfrdg4  36309  brlb  36313  altopthc  36329  altopthd  36330  fvtransport  36390  hfext  36541  ss-ax8  36593  nn0prpw  36691  filnetlem4  36749  df3nandALT2  36768  regsfromregtco  36906  mh-prprimbi  36911  mh-regprimbi  36913  mh-infprim2bi  36915  mh-infprim3bi  36916  bj-sbeq  37393  bj-csbsnlem  37395  bj-elsngl  37460  bj-eltag  37469  bj-tagex  37479  bj-projun  37486  bj-reabeq  37519  bj-disj2r  37520  bj-axseprep  37566  bj-restuni  37594  bj-elid6  37669  bj-eldiag  37675  bj-eldiag2  37676  topdifinffinlem  37848  relowlpssretop  37865  fvineqsneq  37913  wl-3xorbi  37974  wl-2mintru1  37991  wl-df3maxtru1  37993  wl-dfclab  38095  phpreu  38110  poimirlem24  38150  poimirlem26  38152  poimirlem30  38156  areacirclem5  38218  isbnd2  38289  sbcalf  38620  sbcexf  38621  sbccom2  38631  sbccom2f  38632  sbccom2fi  38633  csbcom2fi  38634  anan  38741  br1cnvinxp  38765  idinxpssinxp2  38830  ineleq  38860  brabidgaw  38879  brabidga  38880  inxpxrn  38924  rnxrn  38927  dfsucmap3  38969  cossssid2  39064  cossssid3  39065  cosscnvssid3  39072  dfeldisj3  39317  dfeldisj4  39318  antisymrelres  39372  dfmembpart2  39379  mpet3  39456  cpet2  39457  prtlem70  39488  prtlem16  39500  ishlat2  39984  pmapglb  40401  polval2N  40537  dicelval3  41811  mapdordlem1a  42265  redvmptabs  42976  fimgmcyclem  43158  fimgmcyc  43159  prjspeclsp  43201  sn-isghm  43262  abbibw  43266  fz1eqin  43357  7rexfrabdioph  43384  rmydioph  43598  dford4  43613  areaquad  43800  onsupmaxb  43823  onov0suclim  43858  nnoeomeqom  43896  tfsconcat0i  43929  faosnf0.11b  44010  ifpan23  44043  ifpdfnan  44069  ifpdfxor  44070  ifpidg  44074  ifpid1g  44077  ifpim123g  44083  ifp1bi  44085  ifpimimb  44087  ifpororb  44088  ifpbibib  44093  rp-fakeuninass  44099  dfsucon  44106  minregex  44117  cllem0  44149  rababg  44157  elmapintrab  44159  elmapintab  44179  undmrnresiss  44187  dfxor4  44349  dfhe3  44358  dffrege115  44561  frege131  44577  frege133  44579  clsk1indlem4  44627  clsk1indlem1  44628  expandrexn  44860  rr-groth  44868  rr-grothshortbi  44872  undisjrab  44875  pm13.196a  44983  eelT11  45274  eelTT1  45277  eelT01  45278  eel0T1  45279  uunTT1  45360  uunTT1p1  45361  uunTT1p2  45362  uunT11  45363  uunT11p1  45364  uunT11p2  45365  uun111  45372  xpwf  45532  permaxinf2lem  45580  permac8prim  45582  ssrabf  45691  rabssf  45696  disjinfi  45769  elicores  46108  fourierdlem42  46722  iundjiun  47033  2reu7  47704  2reu8  47705  2reu8i  47706  dfdfat2  47721  aovov0bi  47789  afv2orxorb  47821  afv2ndeffv0  47853  ichcircshi  48059  ichan  48060  icheq  48067  ichal  48071  prpair  48106  prproropf1olem0  48107  257prm  48169  fmtno4prmfac  48180  nnsum4primeseven  48421  nnsum4primesevenALTV  48422  clnbgrel  48449  isubgr3stgrlem4  48590  usgrexmpl2nb1  48653  usgrexmpl2nb2  48654  gpgprismgr4cycllem10  48725  uspgrsprf1  48768  rrx2xpref1o  49350  iinxp  49461  resinsn  49502  resinsnALT  49503  0funcALT  49718  catcsect  50028  isthincd2  50067  aacllem  50431