Theorem 3bitri 297

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 275	. 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:  bibi1i  338  pm5.32  573  biadan  819  orbi1i  913  orass  921  or32  925  cases  1042  dn1  1057  3anidm  1103  an33rean  1482  nanbi  1496  excxor  1512  cadan  1605  cadcomb  1609  nic-axALT  1670  tbw-bijust  1694  rb-bijust  1745  nf2  1781  19.43  1879  19.43OLD  1880  3exdistr  1957  19.12vvv  1985  excom13  2161  sbcom2  2170  sbco4OLD  2172  sbn  2278  sbnf  2310  19.12vv  2347  eeeanv  2350  ee4anv  2351  2sb8ef  2356  sbel2x  2476  2sb8e  2532  dfmo  2593  sb8eulem  2595  2mo2  2644  2eu7  2655  2eu8  2656  sbabel  2935  r19.23v  3180  2ralor  3228  rexcomOLD  3288  ralcom13OLD  3292  rexcom13  3293  cbvreuwOLD  3412  cbvreu  3424  rabrabi  3452  cgsex4g  3525  ceqsex2  3534  ceqsex2v  3535  ceqsex3v  3536  ceqsex4v  3537  ceqsex6v  3538  ceqsex8v  3539  ralrab2  3706  rexrab2  3708  reu2  3733  rmo4  3738  reu8  3741  rmo3f  3742  2reu5lem3  3765  sbcimdv  3864  reu8nf  3885  rmo2  3895  rmo3  3897  rmoanim  3902  ss2rab  4080  rabss  4081  ssrab  4082  dfdif3OLD  4127  symdifass  4267  dfss4  4274  undi  4290  indifdi  4299  undif3  4305  reuun2  4330  difin0ss  4378  disj  4455  disj4  4464  rabsssn  4672  disjsn  4715  snssb  4786  raldifsni  4799  ssunpr  4838  sspr  4839  sstp  4840  uni0b  4937  uni0c  4938  ssint  4968  intprg  4985  iunssf  5048  iunss  5049  iundif2  5078  disjor  5129  nfnid  5380  reusv2lem4  5406  ssextss  5463  exss  5473  eqvinop  5497  sbcop  5499  opcom  5510  opeqpr  5514  brtp  5532  brabsb  5540  opelopabf  5554  dfid3  5585  pofun  5614  opeliunxp  5755  xpiundi  5758  brinxp2  5765  reliun  5828  exopxfr  5856  cnvuni  5899  dmopab3  5932  rnep  5939  dmxp  5941  rnopab3  5969  elres  6039  elsnres  6040  elrid  6065  cnvsym  6134  cnvsymOLD  6135  asymref2  6139  intirr  6140  cnvopab  6159  xpeq0  6181  difxp  6185  xpdifid  6189  ssrnres  6199  dminxp  6201  dfrel4v  6211  elid  6220  dmsnn0  6228  imaco  6272  rnco  6273  coeq0  6276  resssxp  6291  dfpo2  6317  snres0  6319  sspred  6331  frpoind  6364  wfiOLD  6373  sb8iota  6526  dffun2OLDOLD  6574  fun11  6641  isarep1  6656  isarep1OLD  6657  dff1o4  6856  opabiota  6990  fvopab5  7048  eqfnfv3  7052  fvn0ssdmfun  7093  fnressn  7177  f13dfv  7293  dff1o6  7294  fliftel  7328  oprabidw  7461  oprabid  7462  eloprabga  7540  mpo2eqb  7564  ralrnmpo  7571  uniuni  7780  dflim3  7867  dfom2  7888  elxp4  7944  elxp5  7945  opabex3d  7988  opabex3rd  7989  opabex3  7990  el2xptp  8058  fsplit  8140  xporderlem  8150  ralxp3f  8160  frpoins3xpg  8163  poxp2  8166  suppvalbr  8187  dfrecs3  8410  dfrecs3OLD  8411  tz7.48lem  8479  seqomlem2  8489  oaord  8583  oeeu  8639  nnaord  8655  ecid  8820  mptelixpg  8973  elixpsn  8975  xpsnen  9093  xpcomco  9100  xpassen  9104  omxpenlem  9111  dom0OLD  9141  modom  9277  brttrcl2  9751  ttrcltr  9753  rnttrcl  9759  frind  9787  tz9.12lem3  9826  rankxpsuc  9919  cp  9928  cardprclem  10016  infxpenlem  10050  dfac5lem1  10160  dfac5lem2  10161  dfac5lem5  10164  dfac10c  10176  kmlem3  10190  kmlem12  10199  kmlem13  10200  kmlem14  10201  kmlem15  10202  ackbij2  10279  cf0  10288  cflim2  10300  dffin7-2  10435  dfacfin7  10436  fin1a2lem12  10448  axdc3lem3  10489  cfpwsdom  10621  recmulnq  11001  genpass  11046  psslinpr  11068  suplem2pr  11090  opelreal  11167  ltxrlt  11328  addrid  11438  elnn0  12525  elxnn0  12598  elnn0z  12623  nnwos  12954  elxr  13155  xrnepnf  13157  elfzuzb  13554  4fvwrd4  13684  preduz  13686  elfzo2  13698  ssnn0fi  14022  sqeqori  14249  xpcogend  15009  cotr2g  15011  fsumcom2  15806  modfsummod  15826  fprodcom2  16016  rpnnen2lem12  16257  gcdcllem1  16532  isprm2  16715  isprm7  16741  pythagtriplem2  16850  infpn2  16946  4sqlem12  16989  initoid  18054  termoid  18055  eldmcoa  18118  oduposb  18386  gsumwspan  18871  smndex1basss  18930  smndex1mgm  18932  isnsg2  19186  isnsg4  19197  cycsubmel  19230  efgcpbllemb  19787  dmdprd  20032  dprdval  20037  dprdw  20044  dprd2d2  20078  dfrhm2  20490  brric2  20522  issubrg  20587  isdomn5  20726  islmim  21078  lbsextlem2  21178  cnfldfun  21395  cnfldfunOLD  21408  pzriprnglem3  21511  pjfval2  21746  opsrtoslem1  22096  ntreq0  23100  cmpcov2  23413  cmpsub  23423  2ndcdisj  23479  unisngl  23550  txbas  23590  elpt  23595  txkgen  23675  xkococn  23683  fbun  23863  trfil2  23910  fin1aufil  23955  alexsubALTlem3  24072  cnextcn  24090  qustgplem  24144  eltsms  24156  ustn0  24244  fmucndlem  24315  metrest  24552  restmetu  24598  isclmp  25143  srabn  25407  ellogdm  26695  1cubr  26899  leibpilem2  26998  dmarea  27014  vmasum  27274  dchrelbas2  27295  2lgslem4  27464  nosupbnd1lem4  27770  nosupbnd2lem1  27774  slenlt  27811  madeval2  27906  made0  27926  tgcgr4  28553  ltgov  28619  axlowdimlem13  28983  axeuclidlem  28991  numedglnl  29175  nbupgrres  29395  vtxd0nedgb  29520  rusgrprc  29622  usgr2pth0  29797  wspthsnwspthsnon  29945  isclwwlk  30012  clwwlkn1  30069  clwwlkn2  30072  clwwlknonel  30123  3pthdlem1  30192  iseupthf1o  30230  frgr3v  30303  fusgr2wsp2nb  30362  frgrregord013  30423  h2hcau  31007  h2hlm  31008  shlesb1i  31414  shne0i  31476  chnlei  31513  cmbr2i  31624  pjneli  31751  ho02i  31857  adjsym  31861  adjeu  31917  lnopeqi  32036  largei  32295  atoml2i  32411  cdj3lem3b  32468  or3di  32487  mo5f  32516  dmrab  32524  rabsspr  32528  rabsstp  32529  disjnf  32589  disjorf  32598  ssrelf  32634  ofpreima  32681  disjdsct  32717  1stpreima  32721  2ndpreima  32722  f1od2  32738  xrdifh  32788  nndiffz1  32794  prmidl0  33457  zarclsun  33830  ordtconnlem1  33884  ind1a  33999  measiuns  34197  elunirnmbfm  34232  eulerpartlemr  34355  eulerpartlemgh  34359  eulerpartlemn  34362  ballotlemodife  34478  bnj250  34693  bnj334  34705  bnj345  34706  bnj89  34713  bnj115  34717  bnj919  34759  bnj1304  34811  bnj92  34854  bnj124  34863  bnj126  34865  bnj154  34870  bnj155  34871  bnj523  34879  bnj526  34880  bnj540  34884  bnj581  34900  bnj916  34925  bnj929  34928  bnj964  34935  bnj978  34941  bnj983  34943  bnj1039  34963  bnj1040  34964  bnj1123  34978  bnj1128  34982  bnj1398  35026  lfuhgr3  35103  cvmlift2lem1  35286  satfv0  35342  satf0  35356  satf0op  35361  satffunlem  35385  satffunlem1lem1  35386  satffunlem2lem1  35388  elmthm  35560  quad3  35654  3orit  35695  dftr6  35730  eldm3  35740  elrn3  35741  elima4  35756  19.12b  35782  brtxp  35861  brtxp2  35862  brpprod  35866  brpprod3a  35867  elfix  35884  dffix2  35886  ellimits  35891  sscoid  35894  dffun10  35895  elfuns  35896  elsingles  35899  brimg  35918  brapply  35919  brsuccf  35922  funpartlem  35923  brrestrict  35930  dfrecs2  35931  dfrdg4  35932  brlb  35936  altopthc  35952  altopthd  35953  fvtransport  36013  hfext  36164  ss-ax8  36207  nn0prpw  36305  filnetlem4  36363  df3nandALT2  36382  bj-sbeq  36883  bj-csbsnlem  36885  bj-elsngl  36950  bj-eltag  36959  bj-tagex  36969  bj-projun  36976  bj-reabeq  37009  bj-disj2r  37010  bj-restuni  37079  bj-elid6  37152  bj-eldiag  37158  bj-eldiag2  37159  topdifinffinlem  37329  relowlpssretop  37346  fvineqsneq  37394  wl-3xorbi  37455  wl-2mintru1  37472  wl-df3maxtru1  37474  wl-dfclab  37576  phpreu  37590  poimirlem24  37630  poimirlem26  37632  poimirlem30  37636  areacirclem5  37698  isbnd2  37769  sbcalf  38100  sbcexf  38101  sbccom2  38111  sbccom2f  38112  sbccom2fi  38113  csbcom2fi  38114  anan  38209  br1cnvinxp  38237  idinxpssinxp2  38299  ineleq  38335  brabidgaw  38346  brabidga  38347  inxpxrn  38376  rnxrn  38379  cossssid2  38449  cossssid3  38450  cosscnvssid3  38457  dfeldisj3  38700  dfeldisj4  38701  antisymrelres  38744  dfmembpart2  38751  mpet3  38817  cpet2  38818  prtlem70  38838  prtlem16  38850  ishlat2  39334  pmapglb  39752  polval2N  39888  dicelval3  41162  mapdordlem1a  41616  redvmptabs  42368  fimgmcyclem  42519  fimgmcyc  42520  prjspeclsp  42598  sn-isghm  42659  abbibw  42663  fz1eqin  42756  7rexfrabdioph  42787  rmydioph  43002  dford4  43017  areaquad  43204  onsupmaxb  43227  onov0suclim  43263  nnoeomeqom  43301  tfsconcat0i  43334  faosnf0.11b  43416  ifpan23  43449  ifpdfnan  43475  ifpdfxor  43476  ifpidg  43480  ifpid1g  43483  ifpim123g  43489  ifp1bi  43491  ifpimimb  43493  ifpororb  43494  ifpbibib  43499  rp-fakeuninass  43505  dfsucon  43512  minregex  43523  cllem0  43555  rababg  43563  elmapintrab  43565  elmapintab  43585  undmrnresiss  43593  dfxor4  43755  dfhe3  43764  dffrege115  43967  frege131  43983  frege133  43985  clsk1indlem4  44033  clsk1indlem1  44034  expandrexn  44286  rr-groth  44294  rr-grothshortbi  44298  undisjrab  44301  pm13.196a  44409  eelT11  44704  eelTT1  44707  eelT01  44708  eel0T1  44709  uunTT1  44790  uunTT1p1  44791  uunTT1p2  44792  uunT11  44793  uunT11p1  44794  uunT11p2  44795  uun111  44802  xpwf  44938  ssrabf  45053  rabssf  45058  disjinfi  45134  elicores  45485  fourierdlem42  46104  iundjiun  46415  2reu7  47060  2reu8  47061  2reu8i  47062  dfdfat2  47077  aovov0bi  47145  afv2orxorb  47177  afv2ndeffv0  47209  ichcircshi  47378  ichan  47379  icheq  47386  ichal  47390  prpair  47425  prproropf1olem0  47426  257prm  47485  fmtno4prmfac  47496  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  clnbgrel  47752  isubgr3stgrlem4  47871  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  uspgrsprf1  47990  opeliun2xp  48177  rrx2xpref1o  48567  isthincd2  48837  aacllem  49031