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  1994  sbco4  2103  excom13  2165  sbcom2  2174  sbco4OLD  2176  sbn  2280  sbnf  2311  19.12vv  2345  eeeanv  2348  ee4anv  2349  ee4anvOLD  2350  2sb8ef  2354  sbel2x  2472  2sb8e  2528  dfmo  2589  sb8eulem  2591  2mo2  2640  2eu7  2651  2eu8  2652  sbabel  2924  3r19.43  3098  r19.23v  3156  2ralor  3203  ralcom13OLD  3262  rexcom13  3263  cbvreu  3388  rabrabi  3416  cgsex4g  3485  ceqsex2  3492  ceqsex2v  3493  ceqsex3v  3494  ceqsex4v  3495  ceqsex6v  3496  ceqsex8v  3497  ralrab2  3660  rexrab2  3662  reu2  3687  rmo4  3692  reu8  3695  rmo3f  3696  2reu5lem3  3719  sbcimdv  3813  reu8nf  3831  rmo2  3841  rmo3  3843  rmoanim  3848  ss2rab  4024  rabss  4025  ssrab  4026  dfdif3OLD  4071  symdifass  4215  dfss4  4222  undi  4238  indifdi  4247  undif3  4253  reuun2  4278  difin0ss  4326  disj  4403  disj4  4412  rabsssn  4622  disjsn  4665  snssb  4736  raldifsni  4749  ssunpr  4788  sspr  4789  sstp  4790  uni0b  4887  uni0c  4888  ssint  4917  intprg  4934  iunssf  4996  iunss  4997  iundif2  5026  disjor  5077  nfnid  5317  reusv2lem4  5343  ssextss  5400  exss  5410  eqvinop  5434  sbcop  5436  opcom  5448  opeqpr  5452  brtp  5470  brabsb  5478  opelopabf  5492  dfid3  5521  pofun  5549  opeliunxp  5690  opeliun2xp  5691  xpiundi  5694  brinxp2  5701  reliun  5763  exopxfr  5790  cnvuni  5833  dmopab3  5866  rnep  5873  dmxp  5875  rnopab3  5902  elres  5975  elsnres  5976  elrid  6001  cnvsym  6067  asymref2  6070  intirr  6071  cnvopab  6090  xpeq0  6113  difxp  6117  xpdifid  6121  ssrnres  6131  dminxp  6133  dfrel4v  6143  elid  6152  dmsnn0  6160  imaco  6204  rnco  6205  coeq0  6208  resssxp  6222  dfpo2  6248  snres0  6250  sspred  6262  frpoind  6294  sb8iota  6453  fun11  6560  isarep1  6575  dff1o4  6776  opabiota  6909  fvopab5  6967  eqfnfv3  6971  fvn0ssdmfun  7012  fnressn  7096  f13dfv  7215  dff1o6  7216  fliftel  7250  oprabidw  7384  oprabid  7385  eloprabga  7462  mpo2eqb  7485  ralrnmpo  7492  uniuni  7702  dflim3  7787  dfom2  7808  elxp4  7862  elxp5  7863  opabex3d  7907  opabex3rd  7908  opabex3  7909  el2xptp  7977  fsplit  8057  xporderlem  8067  ralxp3f  8077  frpoins3xpg  8080  poxp2  8083  suppvalbr  8104  dfrecs3  8302  tz7.48lem  8370  seqomlem2  8380  oaord  8472  oeeu  8528  nnaord  8544  ecid  8714  mptelixpg  8869  elixpsn  8871  xpsnen  8985  xpcomco  8991  xpassen  8995  omxpenlem  9002  modom  9150  brttrcl2  9629  ttrcltr  9631  rnttrcl  9637  frind  9665  tz9.12lem3  9704  rankxpsuc  9797  cp  9806  cardprclem  9894  infxpenlem  9926  dfac5lem1  10036  dfac5lem2  10037  dfac5lem5  10040  dfac10c  10052  kmlem3  10066  kmlem12  10075  kmlem13  10076  kmlem14  10077  kmlem15  10078  ackbij2  10155  cf0  10164  cflim2  10176  dffin7-2  10311  dfacfin7  10312  fin1a2lem12  10324  axdc3lem3  10365  cfpwsdom  10497  recmulnq  10877  genpass  10922  psslinpr  10944  suplem2pr  10966  opelreal  11043  ltxrlt  11204  addrid  11314  elnn0  12404  elxnn0  12477  elnn0z  12502  nnwos  12834  elxr  13036  xrnepnf  13038  elfzuzb  13439  4fvwrd4  13569  preduz  13571  elfzo2  13583  ssnn0fi  13910  sqeqori  14139  xpcogend  14899  cotr2g  14901  fsumcom2  15699  modfsummod  15719  fprodcom2  15909  rpnnen2lem12  16152  gcdcllem1  16428  isprm2  16611  isprm7  16637  pythagtriplem2  16747  infpn2  16843  4sqlem12  16886  initoid  17926  termoid  17927  eldmcoa  17990  oduposb  18251  gsumwspan  18738  smndex1basss  18797  smndex1mgm  18799  isnsg2  19053  isnsg4  19064  cycsubmel  19097  efgcpbllemb  19652  dmdprd  19897  dprdval  19902  dprdw  19909  dprd2d2  19943  dfrhm2  20377  brric2  20409  issubrg  20474  isdomn5  20613  islmim  20984  lbsextlem2  21084  cnfldfun  21293  cnfldfunOLD  21306  pzriprnglem3  21408  pjfval2  21634  opsrtoslem1  21978  ntreq0  22980  cmpcov2  23293  cmpsub  23303  2ndcdisj  23359  unisngl  23430  txbas  23470  elpt  23475  txkgen  23555  xkococn  23563  fbun  23743  trfil2  23790  fin1aufil  23835  alexsubALTlem3  23952  cnextcn  23970  qustgplem  24024  eltsms  24036  ustn0  24124  fmucndlem  24194  metrest  24428  restmetu  24474  isclmp  25013  srabn  25276  ellogdm  26564  1cubr  26768  leibpilem2  26867  dmarea  26883  vmasum  27143  dchrelbas2  27164  2lgslem4  27333  nosupbnd1lem4  27639  nosupbnd2lem1  27643  slenlt  27680  madeval2  27781  made0  27805  onsiso  28192  onsfi  28270  tgcgr4  28494  ltgov  28560  axlowdimlem13  28917  axeuclidlem  28925  numedglnl  29107  nbupgrres  29327  vtxd0nedgb  29452  rusgrprc  29554  usgr2pth0  29728  wspthsnwspthsnon  29879  isclwwlk  29946  clwwlkn1  30003  clwwlkn2  30006  clwwlknonel  30057  3pthdlem1  30126  iseupthf1o  30164  frgr3v  30237  fusgr2wsp2nb  30296  frgrregord013  30357  h2hcau  30941  h2hlm  30942  shlesb1i  31348  shne0i  31410  chnlei  31447  cmbr2i  31558  pjneli  31685  ho02i  31791  adjsym  31795  adjeu  31851  lnopeqi  31970  largei  32229  atoml2i  32345  cdj3lem3b  32402  or3di  32421  mo5f  32451  dmrab  32459  rabsspr  32463  rabsstp  32464  disjnf  32532  disjorf  32541  ssrelf  32576  ofpreima  32622  disjdsct  32659  1stpreima  32663  2ndpreima  32664  f1od2  32677  xrdifh  32736  nndiffz1  32742  ind1a  32815  prmidl0  33400  zarclsun  33839  ordtconnlem1  33893  measiuns  34186  elunirnmbfm  34221  eulerpartlemr  34344  eulerpartlemgh  34348  eulerpartlemn  34351  ballotlemodife  34468  bnj250  34670  bnj334  34682  bnj345  34683  bnj89  34690  bnj115  34694  bnj919  34736  bnj1304  34788  bnj92  34831  bnj124  34840  bnj126  34842  bnj154  34847  bnj155  34848  bnj523  34856  bnj526  34857  bnj540  34861  bnj581  34877  bnj916  34902  bnj929  34905  bnj964  34912  bnj978  34918  bnj983  34920  bnj1039  34940  bnj1040  34941  bnj1123  34955  bnj1128  34959  bnj1398  35003  lfuhgr3  35095  cvmlift2lem1  35277  satfv0  35333  satf0  35347  satf0op  35352  satffunlem  35376  satffunlem1lem1  35377  satffunlem2lem1  35379  elmthm  35551  quad3  35645  3orit  35691  dftr6  35726  eldm3  35736  elrn3  35737  elima4  35751  19.12b  35777  brtxp  35856  brtxp2  35857  brpprod  35861  brpprod3a  35862  elfix  35879  dffix2  35881  ellimits  35886  sscoid  35889  dffun10  35890  elfuns  35891  elsingles  35894  brimg  35913  brapply  35914  brsuccf  35917  funpartlem  35918  brrestrict  35925  dfrecs2  35926  dfrdg4  35927  brlb  35931  altopthc  35947  altopthd  35948  fvtransport  36008  hfext  36159  ss-ax8  36201  nn0prpw  36299  filnetlem4  36357  df3nandALT2  36376  bj-sbeq  36877  bj-csbsnlem  36879  bj-elsngl  36944  bj-eltag  36953  bj-tagex  36963  bj-projun  36970  bj-reabeq  37003  bj-disj2r  37004  bj-restuni  37073  bj-elid6  37146  bj-eldiag  37152  bj-eldiag2  37153  topdifinffinlem  37323  relowlpssretop  37340  fvineqsneq  37388  wl-3xorbi  37449  wl-2mintru1  37466  wl-df3maxtru1  37468  wl-dfclab  37572  phpreu  37586  poimirlem24  37626  poimirlem26  37628  poimirlem30  37632  areacirclem5  37694  isbnd2  37765  sbcalf  38096  sbcexf  38097  sbccom2  38107  sbccom2f  38108  sbccom2fi  38109  csbcom2fi  38110  anan  38205  br1cnvinxp  38233  idinxpssinxp2  38294  ineleq  38324  brabidgaw  38335  brabidga  38336  inxpxrn  38369  rnxrn  38372  cossssid2  38447  cossssid3  38448  cosscnvssid3  38455  dfeldisj3  38699  dfeldisj4  38700  antisymrelres  38743  dfmembpart2  38750  mpet3  38816  cpet2  38817  prtlem70  38838  prtlem16  38850  ishlat2  39334  pmapglb  39752  polval2N  39888  dicelval3  41162  mapdordlem1a  41616  redvmptabs  42336  fimgmcyclem  42509  fimgmcyc  42510  prjspeclsp  42588  sn-isghm  42649  abbibw  42653  fz1eqin  42745  7rexfrabdioph  42776  rmydioph  42990  dford4  43005  areaquad  43192  onsupmaxb  43215  onov0suclim  43250  nnoeomeqom  43288  tfsconcat0i  43321  faosnf0.11b  43403  ifpan23  43436  ifpdfnan  43462  ifpdfxor  43463  ifpidg  43467  ifpid1g  43470  ifpim123g  43476  ifp1bi  43478  ifpimimb  43480  ifpororb  43481  ifpbibib  43486  rp-fakeuninass  43492  dfsucon  43499  minregex  43510  cllem0  43542  rababg  43550  elmapintrab  43552  elmapintab  43572  undmrnresiss  43580  dfxor4  43742  dfhe3  43751  dffrege115  43954  frege131  43970  frege133  43972  clsk1indlem4  44020  clsk1indlem1  44021  expandrexn  44267  rr-groth  44275  rr-grothshortbi  44279  undisjrab  44282  pm13.196a  44390  eelT11  44683  eelTT1  44686  eelT01  44687  eel0T1  44688  uunTT1  44769  uunTT1p1  44770  uunTT1p2  44771  uunT11  44772  uunT11p1  44773  uunT11p2  44774  uun111  44781  xpwf  44941  permaxinf2lem  44989  permac8prim  44991  ssrabf  45095  rabssf  45100  disjinfi  45173  elicores  45518  fourierdlem42  46134  iundjiun  46445  2reu7  47099  2reu8  47100  2reu8i  47101  dfdfat2  47116  aovov0bi  47184  afv2orxorb  47216  afv2ndeffv0  47248  ichcircshi  47442  ichan  47443  icheq  47450  ichal  47454  prpair  47489  prproropf1olem0  47490  257prm  47549  fmtno4prmfac  47560  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  clnbgrel  47816  isubgr3stgrlem4  47957  usgrexmpl2nb1  48020  usgrexmpl2nb2  48021  gpgprismgr4cycllem10  48092  uspgrsprf1  48135  rrx2xpref1o  48707  iinxp  48819  resinsn  48860  resinsnALT  48861  0funcALT  49077  catcsect  49387  isthincd2  49426  aacllem  49790