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  2355  sbel2x  2473  2sb8e  2529  dfmo  2590  sb8eulem  2592  2mo2  2641  2eu7  2652  2eu8  2653  sbabel  2925  3r19.43  3103  r19.23v  3162  2ralor  3212  rexcomOLD  3268  ralcom13OLD  3272  rexcom13  3273  cbvreuwOLD  3389  cbvreu  3400  rabrabi  3428  cgsex4g  3497  ceqsex2  3504  ceqsex2v  3505  ceqsex3v  3506  ceqsex4v  3507  ceqsex6v  3508  ceqsex8v  3509  ralrab2  3672  rexrab2  3674  reu2  3699  rmo4  3704  reu8  3707  rmo3f  3708  2reu5lem3  3731  sbcimdv  3825  reu8nf  3843  rmo2  3853  rmo3  3855  rmoanim  3860  ss2rab  4037  rabss  4038  ssrab  4039  dfdif3OLD  4084  symdifass  4228  dfss4  4235  undi  4251  indifdi  4260  undif3  4266  reuun2  4291  difin0ss  4339  disj  4416  disj4  4425  rabsssn  4635  disjsn  4678  snssb  4749  raldifsni  4762  ssunpr  4801  sspr  4802  sstp  4803  uni0b  4900  uni0c  4901  ssint  4931  intprg  4948  iunssf  5011  iunss  5012  iundif2  5041  disjor  5092  nfnid  5333  reusv2lem4  5359  ssextss  5416  exss  5426  eqvinop  5450  sbcop  5452  opcom  5464  opeqpr  5468  brtp  5486  brabsb  5494  opelopabf  5508  dfid3  5539  pofun  5567  opeliunxp  5708  opeliun2xp  5709  xpiundi  5712  brinxp2  5719  reliun  5782  exopxfr  5810  cnvuni  5853  dmopab3  5886  rnep  5893  dmxp  5895  rnopab3  5923  elres  5994  elsnres  5995  elrid  6020  cnvsym  6088  cnvsymOLD  6089  asymref2  6093  intirr  6094  cnvopab  6113  xpeq0  6136  difxp  6140  xpdifid  6144  ssrnres  6154  dminxp  6156  dfrel4v  6166  elid  6175  dmsnn0  6183  imaco  6227  rnco  6228  coeq0  6231  resssxp  6246  dfpo2  6272  snres0  6274  sspred  6286  frpoind  6318  sb8iota  6478  dffun2OLDOLD  6526  fun11  6593  isarep1  6609  isarep1OLD  6610  dff1o4  6811  opabiota  6946  fvopab5  7004  eqfnfv3  7008  fvn0ssdmfun  7049  fnressn  7133  f13dfv  7252  dff1o6  7253  fliftel  7287  oprabidw  7421  oprabid  7422  eloprabga  7501  mpo2eqb  7524  ralrnmpo  7531  uniuni  7741  dflim3  7826  dfom2  7847  elxp4  7901  elxp5  7902  opabex3d  7947  opabex3rd  7948  opabex3  7949  el2xptp  8017  fsplit  8099  xporderlem  8109  ralxp3f  8119  frpoins3xpg  8122  poxp2  8125  suppvalbr  8146  dfrecs3  8344  tz7.48lem  8412  seqomlem2  8422  oaord  8514  oeeu  8570  nnaord  8586  ecid  8756  mptelixpg  8911  elixpsn  8913  xpsnen  9029  xpcomco  9036  xpassen  9040  omxpenlem  9047  modom  9198  brttrcl2  9674  ttrcltr  9676  rnttrcl  9682  frind  9710  tz9.12lem3  9749  rankxpsuc  9842  cp  9851  cardprclem  9939  infxpenlem  9973  dfac5lem1  10083  dfac5lem2  10084  dfac5lem5  10087  dfac10c  10099  kmlem3  10113  kmlem12  10122  kmlem13  10123  kmlem14  10124  kmlem15  10125  ackbij2  10202  cf0  10211  cflim2  10223  dffin7-2  10358  dfacfin7  10359  fin1a2lem12  10371  axdc3lem3  10412  cfpwsdom  10544  recmulnq  10924  genpass  10969  psslinpr  10991  suplem2pr  11013  opelreal  11090  ltxrlt  11251  addrid  11361  elnn0  12451  elxnn0  12524  elnn0z  12549  nnwos  12881  elxr  13083  xrnepnf  13085  elfzuzb  13486  4fvwrd4  13616  preduz  13618  elfzo2  13630  ssnn0fi  13957  sqeqori  14186  xpcogend  14947  cotr2g  14949  fsumcom2  15747  modfsummod  15767  fprodcom2  15957  rpnnen2lem12  16200  gcdcllem1  16476  isprm2  16659  isprm7  16685  pythagtriplem2  16795  infpn2  16891  4sqlem12  16934  initoid  17970  termoid  17971  eldmcoa  18034  oduposb  18295  gsumwspan  18780  smndex1basss  18839  smndex1mgm  18841  isnsg2  19095  isnsg4  19106  cycsubmel  19139  efgcpbllemb  19692  dmdprd  19937  dprdval  19942  dprdw  19949  dprd2d2  19983  dfrhm2  20390  brric2  20422  issubrg  20487  isdomn5  20626  islmim  20976  lbsextlem2  21076  cnfldfun  21285  cnfldfunOLD  21298  pzriprnglem3  21400  pjfval2  21625  opsrtoslem1  21969  ntreq0  22971  cmpcov2  23284  cmpsub  23294  2ndcdisj  23350  unisngl  23421  txbas  23461  elpt  23466  txkgen  23546  xkococn  23554  fbun  23734  trfil2  23781  fin1aufil  23826  alexsubALTlem3  23943  cnextcn  23961  qustgplem  24015  eltsms  24027  ustn0  24115  fmucndlem  24185  metrest  24419  restmetu  24465  isclmp  25004  srabn  25267  ellogdm  26555  1cubr  26759  leibpilem2  26858  dmarea  26874  vmasum  27134  dchrelbas2  27155  2lgslem4  27324  nosupbnd1lem4  27630  nosupbnd2lem1  27634  slenlt  27671  madeval2  27768  made0  27792  onsiso  28176  onsfi  28254  tgcgr4  28465  ltgov  28531  axlowdimlem13  28888  axeuclidlem  28896  numedglnl  29078  nbupgrres  29298  vtxd0nedgb  29423  rusgrprc  29525  usgr2pth0  29702  wspthsnwspthsnon  29853  isclwwlk  29920  clwwlkn1  29977  clwwlkn2  29980  clwwlknonel  30031  3pthdlem1  30100  iseupthf1o  30138  frgr3v  30211  fusgr2wsp2nb  30270  frgrregord013  30331  h2hcau  30915  h2hlm  30916  shlesb1i  31322  shne0i  31384  chnlei  31421  cmbr2i  31532  pjneli  31659  ho02i  31765  adjsym  31769  adjeu  31825  lnopeqi  31944  largei  32203  atoml2i  32319  cdj3lem3b  32376  or3di  32395  mo5f  32425  dmrab  32433  rabsspr  32437  rabsstp  32438  disjnf  32506  disjorf  32515  ssrelf  32550  ofpreima  32596  disjdsct  32633  1stpreima  32637  2ndpreima  32638  f1od2  32651  xrdifh  32710  nndiffz1  32716  ind1a  32789  prmidl0  33428  zarclsun  33867  ordtconnlem1  33921  measiuns  34214  elunirnmbfm  34249  eulerpartlemr  34372  eulerpartlemgh  34376  eulerpartlemn  34379  ballotlemodife  34496  bnj250  34698  bnj334  34710  bnj345  34711  bnj89  34718  bnj115  34722  bnj919  34764  bnj1304  34816  bnj92  34859  bnj124  34868  bnj126  34870  bnj154  34875  bnj155  34876  bnj523  34884  bnj526  34885  bnj540  34889  bnj581  34905  bnj916  34930  bnj929  34933  bnj964  34940  bnj978  34946  bnj983  34948  bnj1039  34968  bnj1040  34969  bnj1123  34983  bnj1128  34987  bnj1398  35031  lfuhgr3  35114  cvmlift2lem1  35296  satfv0  35352  satf0  35366  satf0op  35371  satffunlem  35395  satffunlem1lem1  35396  satffunlem2lem1  35398  elmthm  35570  quad3  35664  3orit  35710  dftr6  35745  eldm3  35755  elrn3  35756  elima4  35770  19.12b  35796  brtxp  35875  brtxp2  35876  brpprod  35880  brpprod3a  35881  elfix  35898  dffix2  35900  ellimits  35905  sscoid  35908  dffun10  35909  elfuns  35910  elsingles  35913  brimg  35932  brapply  35933  brsuccf  35936  funpartlem  35937  brrestrict  35944  dfrecs2  35945  dfrdg4  35946  brlb  35950  altopthc  35966  altopthd  35967  fvtransport  36027  hfext  36178  ss-ax8  36220  nn0prpw  36318  filnetlem4  36376  df3nandALT2  36395  bj-sbeq  36896  bj-csbsnlem  36898  bj-elsngl  36963  bj-eltag  36972  bj-tagex  36982  bj-projun  36989  bj-reabeq  37022  bj-disj2r  37023  bj-restuni  37092  bj-elid6  37165  bj-eldiag  37171  bj-eldiag2  37172  topdifinffinlem  37342  relowlpssretop  37359  fvineqsneq  37407  wl-3xorbi  37468  wl-2mintru1  37485  wl-df3maxtru1  37487  wl-dfclab  37591  phpreu  37605  poimirlem24  37645  poimirlem26  37647  poimirlem30  37651  areacirclem5  37713  isbnd2  37784  sbcalf  38115  sbcexf  38116  sbccom2  38126  sbccom2f  38127  sbccom2fi  38128  csbcom2fi  38129  anan  38224  br1cnvinxp  38252  idinxpssinxp2  38313  ineleq  38343  brabidgaw  38354  brabidga  38355  inxpxrn  38388  rnxrn  38391  cossssid2  38466  cossssid3  38467  cosscnvssid3  38474  dfeldisj3  38718  dfeldisj4  38719  antisymrelres  38762  dfmembpart2  38769  mpet3  38835  cpet2  38836  prtlem70  38857  prtlem16  38869  ishlat2  39353  pmapglb  39771  polval2N  39907  dicelval3  41181  mapdordlem1a  41635  redvmptabs  42355  fimgmcyclem  42528  fimgmcyc  42529  prjspeclsp  42607  sn-isghm  42668  abbibw  42672  fz1eqin  42764  7rexfrabdioph  42795  rmydioph  43010  dford4  43025  areaquad  43212  onsupmaxb  43235  onov0suclim  43270  nnoeomeqom  43308  tfsconcat0i  43341  faosnf0.11b  43423  ifpan23  43456  ifpdfnan  43482  ifpdfxor  43483  ifpidg  43487  ifpid1g  43490  ifpim123g  43496  ifp1bi  43498  ifpimimb  43500  ifpororb  43501  ifpbibib  43506  rp-fakeuninass  43512  dfsucon  43519  minregex  43530  cllem0  43562  rababg  43570  elmapintrab  43572  elmapintab  43592  undmrnresiss  43600  dfxor4  43762  dfhe3  43771  dffrege115  43974  frege131  43990  frege133  43992  clsk1indlem4  44040  clsk1indlem1  44041  expandrexn  44287  rr-groth  44295  rr-grothshortbi  44299  undisjrab  44302  pm13.196a  44410  eelT11  44703  eelTT1  44706  eelT01  44707  eel0T1  44708  uunTT1  44789  uunTT1p1  44790  uunTT1p2  44791  uunT11  44792  uunT11p1  44793  uunT11p2  44794  uun111  44801  xpwf  44961  permaxinf2lem  45009  permac8prim  45011  ssrabf  45115  rabssf  45120  disjinfi  45193  elicores  45538  fourierdlem42  46154  iundjiun  46465  2reu7  47116  2reu8  47117  2reu8i  47118  dfdfat2  47133  aovov0bi  47201  afv2orxorb  47233  afv2ndeffv0  47265  ichcircshi  47459  ichan  47460  icheq  47467  ichal  47471  prpair  47506  prproropf1olem0  47507  257prm  47566  fmtno4prmfac  47577  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  clnbgrel  47833  isubgr3stgrlem4  47972  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  gpgprismgr4cycllem10  48098  uspgrsprf1  48139  rrx2xpref1o  48711  iinxp  48823  resinsn  48864  resinsnALT  48865  0funcALT  49081  catcsect  49391  isthincd2  49430  aacllem  49794