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  818  orbi1i  913  orass  921  or32  925  cases  1042  dn1  1057  3anidm  1103  an33rean  1485  nanbi  1500  excxor  1516  cadan  1609  cadcomb  1613  nic-axALT  1674  tbw-bijust  1698  rb-bijust  1749  nf2  1785  19.43  1882  19.43OLD  1883  3exdistr  1960  19.12vvv  1988  sbco4  2102  excom13  2164  sbcom2  2173  sbco4OLD  2175  sbn  2280  sbnf  2312  19.12vv  2348  eeeanv  2351  ee4anv  2352  ee4anvOLD  2353  2sb8ef  2358  sbel2x  2478  2sb8e  2534  dfmo  2595  sb8eulem  2597  2mo2  2646  2eu7  2657  2eu8  2658  sbabel  2931  3r19.43  3109  r19.23v  3168  2ralor  3215  rexcomOLD  3272  ralcom13OLD  3276  rexcom13  3277  cbvreuwOLD  3394  cbvreu  3407  rabrabi  3435  cgsex4g  3507  ceqsex2  3514  ceqsex2v  3515  ceqsex3v  3516  ceqsex4v  3517  ceqsex6v  3518  ceqsex8v  3519  ralrab2  3681  rexrab2  3683  reu2  3708  rmo4  3713  reu8  3716  rmo3f  3717  2reu5lem3  3740  sbcimdv  3834  reu8nf  3852  rmo2  3862  rmo3  3864  rmoanim  3869  ss2rab  4046  rabss  4047  ssrab  4048  dfdif3OLD  4093  symdifass  4237  dfss4  4244  undi  4260  indifdi  4269  undif3  4275  reuun2  4300  difin0ss  4348  disj  4425  disj4  4434  rabsssn  4644  disjsn  4687  snssb  4758  raldifsni  4771  ssunpr  4810  sspr  4811  sstp  4812  uni0b  4909  uni0c  4910  ssint  4940  intprg  4957  iunssf  5020  iunss  5021  iundif2  5050  disjor  5101  nfnid  5345  reusv2lem4  5371  ssextss  5428  exss  5438  eqvinop  5462  sbcop  5464  opcom  5476  opeqpr  5480  brtp  5498  brabsb  5506  opelopabf  5520  dfid3  5551  pofun  5579  opeliunxp  5721  opeliun2xp  5722  xpiundi  5725  brinxp2  5732  reliun  5795  exopxfr  5823  cnvuni  5866  dmopab3  5899  rnep  5906  dmxp  5908  rnopab3  5936  elres  6007  elsnres  6008  elrid  6033  cnvsym  6101  cnvsymOLD  6102  asymref2  6106  intirr  6107  cnvopab  6126  xpeq0  6149  difxp  6153  xpdifid  6157  ssrnres  6167  dminxp  6169  dfrel4v  6179  elid  6188  dmsnn0  6196  imaco  6240  rnco  6241  coeq0  6244  resssxp  6259  dfpo2  6285  snres0  6287  sspred  6299  frpoind  6331  wfiOLD  6340  sb8iota  6494  dffun2OLDOLD  6542  fun11  6609  isarep1  6625  isarep1OLD  6626  dff1o4  6825  opabiota  6960  fvopab5  7018  eqfnfv3  7022  fvn0ssdmfun  7063  fnressn  7147  f13dfv  7266  dff1o6  7267  fliftel  7301  oprabidw  7434  oprabid  7435  eloprabga  7514  mpo2eqb  7537  ralrnmpo  7544  uniuni  7754  dflim3  7840  dfom2  7861  elxp4  7916  elxp5  7917  opabex3d  7962  opabex3rd  7963  opabex3  7964  el2xptp  8032  fsplit  8114  xporderlem  8124  ralxp3f  8134  frpoins3xpg  8137  poxp2  8140  suppvalbr  8161  dfrecs3  8384  dfrecs3OLD  8385  tz7.48lem  8453  seqomlem2  8463  oaord  8557  oeeu  8613  nnaord  8629  ecid  8794  mptelixpg  8947  elixpsn  8949  xpsnen  9067  xpcomco  9074  xpassen  9078  omxpenlem  9085  dom0OLD  9115  modom  9250  brttrcl2  9726  ttrcltr  9728  rnttrcl  9734  frind  9762  tz9.12lem3  9801  rankxpsuc  9894  cp  9903  cardprclem  9991  infxpenlem  10025  dfac5lem1  10135  dfac5lem2  10136  dfac5lem5  10139  dfac10c  10151  kmlem3  10165  kmlem12  10174  kmlem13  10175  kmlem14  10176  kmlem15  10177  ackbij2  10254  cf0  10263  cflim2  10275  dffin7-2  10410  dfacfin7  10411  fin1a2lem12  10423  axdc3lem3  10464  cfpwsdom  10596  recmulnq  10976  genpass  11021  psslinpr  11043  suplem2pr  11065  opelreal  11142  ltxrlt  11303  addrid  11413  elnn0  12501  elxnn0  12574  elnn0z  12599  nnwos  12929  elxr  13130  xrnepnf  13132  elfzuzb  13533  4fvwrd4  13663  preduz  13665  elfzo2  13677  ssnn0fi  14001  sqeqori  14230  xpcogend  14991  cotr2g  14993  fsumcom2  15788  modfsummod  15808  fprodcom2  15998  rpnnen2lem12  16241  gcdcllem1  16516  isprm2  16699  isprm7  16725  pythagtriplem2  16835  infpn2  16931  4sqlem12  16974  initoid  18012  termoid  18013  eldmcoa  18076  oduposb  18337  gsumwspan  18822  smndex1basss  18881  smndex1mgm  18883  isnsg2  19137  isnsg4  19148  cycsubmel  19181  efgcpbllemb  19734  dmdprd  19979  dprdval  19984  dprdw  19991  dprd2d2  20025  dfrhm2  20432  brric2  20464  issubrg  20529  isdomn5  20668  islmim  21018  lbsextlem2  21118  cnfldfun  21327  cnfldfunOLD  21340  pzriprnglem3  21442  pjfval2  21667  opsrtoslem1  22011  ntreq0  23013  cmpcov2  23326  cmpsub  23336  2ndcdisj  23392  unisngl  23463  txbas  23503  elpt  23508  txkgen  23588  xkococn  23596  fbun  23776  trfil2  23823  fin1aufil  23868  alexsubALTlem3  23985  cnextcn  24003  qustgplem  24057  eltsms  24069  ustn0  24157  fmucndlem  24227  metrest  24461  restmetu  24507  isclmp  25046  srabn  25310  ellogdm  26598  1cubr  26802  leibpilem2  26901  dmarea  26917  vmasum  27177  dchrelbas2  27198  2lgslem4  27367  nosupbnd1lem4  27673  nosupbnd2lem1  27677  slenlt  27714  madeval2  27809  made0  27829  tgcgr4  28456  ltgov  28522  axlowdimlem13  28879  axeuclidlem  28887  numedglnl  29069  nbupgrres  29289  vtxd0nedgb  29414  rusgrprc  29516  usgr2pth0  29693  wspthsnwspthsnon  29844  isclwwlk  29911  clwwlkn1  29968  clwwlkn2  29971  clwwlknonel  30022  3pthdlem1  30091  iseupthf1o  30129  frgr3v  30202  fusgr2wsp2nb  30261  frgrregord013  30322  h2hcau  30906  h2hlm  30907  shlesb1i  31313  shne0i  31375  chnlei  31412  cmbr2i  31523  pjneli  31650  ho02i  31756  adjsym  31760  adjeu  31816  lnopeqi  31935  largei  32194  atoml2i  32310  cdj3lem3b  32367  or3di  32386  mo5f  32416  dmrab  32424  rabsspr  32428  rabsstp  32429  disjnf  32497  disjorf  32506  ssrelf  32541  ofpreima  32589  disjdsct  32626  1stpreima  32630  2ndpreima  32631  f1od2  32644  xrdifh  32703  nndiffz1  32709  ind1a  32782  prmidl0  33411  zarclsun  33847  ordtconnlem1  33901  measiuns  34194  elunirnmbfm  34229  eulerpartlemr  34352  eulerpartlemgh  34356  eulerpartlemn  34359  ballotlemodife  34476  bnj250  34678  bnj334  34690  bnj345  34691  bnj89  34698  bnj115  34702  bnj919  34744  bnj1304  34796  bnj92  34839  bnj124  34848  bnj126  34850  bnj154  34855  bnj155  34856  bnj523  34864  bnj526  34865  bnj540  34869  bnj581  34885  bnj916  34910  bnj929  34913  bnj964  34920  bnj978  34926  bnj983  34928  bnj1039  34948  bnj1040  34949  bnj1123  34963  bnj1128  34967  bnj1398  35011  lfuhgr3  35088  cvmlift2lem1  35270  satfv0  35326  satf0  35340  satf0op  35345  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  elmthm  35544  quad3  35638  3orit  35679  dftr6  35714  eldm3  35724  elrn3  35725  elima4  35739  19.12b  35765  brtxp  35844  brtxp2  35845  brpprod  35849  brpprod3a  35850  elfix  35867  dffix2  35869  ellimits  35874  sscoid  35877  dffun10  35878  elfuns  35879  elsingles  35882  brimg  35901  brapply  35902  brsuccf  35905  funpartlem  35906  brrestrict  35913  dfrecs2  35914  dfrdg4  35915  brlb  35919  altopthc  35935  altopthd  35936  fvtransport  35996  hfext  36147  ss-ax8  36189  nn0prpw  36287  filnetlem4  36345  df3nandALT2  36364  bj-sbeq  36865  bj-csbsnlem  36867  bj-elsngl  36932  bj-eltag  36941  bj-tagex  36951  bj-projun  36958  bj-reabeq  36991  bj-disj2r  36992  bj-restuni  37061  bj-elid6  37134  bj-eldiag  37140  bj-eldiag2  37141  topdifinffinlem  37311  relowlpssretop  37328  fvineqsneq  37376  wl-3xorbi  37437  wl-2mintru1  37454  wl-df3maxtru1  37456  wl-dfclab  37560  phpreu  37574  poimirlem24  37614  poimirlem26  37616  poimirlem30  37620  areacirclem5  37682  isbnd2  37753  sbcalf  38084  sbcexf  38085  sbccom2  38095  sbccom2f  38096  sbccom2fi  38097  csbcom2fi  38098  anan  38193  br1cnvinxp  38220  idinxpssinxp2  38282  ineleq  38318  brabidgaw  38329  brabidga  38330  inxpxrn  38359  rnxrn  38362  cossssid2  38432  cossssid3  38433  cosscnvssid3  38440  dfeldisj3  38683  dfeldisj4  38684  antisymrelres  38727  dfmembpart2  38734  mpet3  38800  cpet2  38801  prtlem70  38821  prtlem16  38833  ishlat2  39317  pmapglb  39735  polval2N  39871  dicelval3  41145  mapdordlem1a  41599  redvmptabs  42350  fimgmcyclem  42503  fimgmcyc  42504  prjspeclsp  42582  sn-isghm  42643  abbibw  42647  fz1eqin  42739  7rexfrabdioph  42770  rmydioph  42985  dford4  43000  areaquad  43187  onsupmaxb  43210  onov0suclim  43245  nnoeomeqom  43283  tfsconcat0i  43316  faosnf0.11b  43398  ifpan23  43431  ifpdfnan  43457  ifpdfxor  43458  ifpidg  43462  ifpid1g  43465  ifpim123g  43471  ifp1bi  43473  ifpimimb  43475  ifpororb  43476  ifpbibib  43481  rp-fakeuninass  43487  dfsucon  43494  minregex  43505  cllem0  43537  rababg  43545  elmapintrab  43547  elmapintab  43567  undmrnresiss  43575  dfxor4  43737  dfhe3  43746  dffrege115  43949  frege131  43965  frege133  43967  clsk1indlem4  44015  clsk1indlem1  44016  expandrexn  44263  rr-groth  44271  rr-grothshortbi  44275  undisjrab  44278  pm13.196a  44386  eelT11  44679  eelTT1  44682  eelT01  44683  eel0T1  44684  uunTT1  44765  uunTT1p1  44766  uunTT1p2  44767  uunT11  44768  uunT11p1  44769  uunT11p2  44770  uun111  44777  xpwf  44937  permaxinf2lem  44985  ssrabf  45086  rabssf  45091  disjinfi  45164  elicores  45510  fourierdlem42  46126  iundjiun  46437  2reu7  47088  2reu8  47089  2reu8i  47090  dfdfat2  47105  aovov0bi  47173  afv2orxorb  47205  afv2ndeffv0  47237  ichcircshi  47416  ichan  47417  icheq  47424  ichal  47428  prpair  47463  prproropf1olem0  47464  257prm  47523  fmtno4prmfac  47534  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  clnbgrel  47790  isubgr3stgrlem4  47929  usgrexmpl2nb1  47984  usgrexmpl2nb2  47985  gpgprismgr4cycllem10  48051  uspgrsprf1  48070  rrx2xpref1o  48646  iinxp  48757  resinsn  48795  resinsnALT  48796  0funcALT  49001  isthincd2  49271  aacllem  49613