Theorem 3bitri 288

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 266	. 2 ⊢ (𝜓 ↔ 𝜃)
5	1, 4	bitri 266	1 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 197

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 198

This theorem is referenced by:  bibi1i  329  pm5.32  565  an32  628  orbi1i  928  orass  936  or32  940  annotanannotOLD  1025  cases  1056  an3andi  1599  an33rean  1600  nanbi  1608  excxor  1623  cadan  1703  cadcomb  1707  nic-axALT  1754  tbw-bijust  1778  rb-bijust  1829  nf2  1865  19.43  1972  19.43OLD  1973  3exdistr  2049  19.12vvv  2086  excom13  2211  19.12vv  2354  eeeanv  2357  ee4anv  2358  sbn  2550  sb3an  2559  sbnf2  2601  sbcom2  2605  sbel2x  2619  sbco4  2626  2sb8e  2627  mo2v  2639  sb8eu  2666  2mo2  2714  2eu7  2723  2eu8  2724  r19.23v  3211  r19.26-3  3254  ralcom13  3288  rexcom13  3289  cbvreu  3358  ceqsralt  3423  ceqsex2  3438  ceqsex4v  3441  ralrab2  3568  rexrab2  3570  reu2  3592  rmo4  3597  reu8  3600  2reu5lem3  3613  sbc3an  3691  reu8nf  3711  rmo2  3721  rmo3  3723  dfss2  3786  ss2rab  3875  rabss  3876  ssrab  3877  dfdif3  3919  symdifass  4051  dfss4  4060  undi  4076  undif3  4090  difin2  4091  dfnul2  4118  difin0ss  4147  disj  4214  disj4  4223  rabsssn  4408  disjsn  4438  raldifsni  4516  ssunpr  4553  sspr  4554  sstp  4555  uni0b  4657  uni0c  4658  ssint  4685  iunss  4753  iundif2  4779  disjor  4826  nfnid  5045  reusv2lem4  5070  ssextss  5112  eqvinop  5144  opcom  5154  opeqsnOLD  5158  opeqpr  5159  brabsb  5181  opelopabf  5195  dfid3  5220  pofun  5248  opeliunxp  5370  xpiundi  5373  brinxp2  5380  brinxp2OLD  5381  ssrelOLD  5410  reliun  5441  exopxfr  5467  cnvuni  5510  dmopab3  5538  opelresOLD  5607  elres  5638  elresOLD  5639  elsnres  5640  elrid  5662  elid  5664  restidsing  5670  asymref2  5724  intirr  5725  xpeq0  5765  xpdifid  5773  ssrnres  5783  dminxp  5785  dfrel4v  5795  dmsnn0  5811  rnco  5855  coeq0  5858  sspred  5901  wfi  5926  sb8iota  6067  dffun2  6107  fun11  6170  isarep1  6184  dff1o4  6357  opabiota  6478  fvopab5  6527  fvn0ssdmfun  6568  fnressn  6645  f13dfv  6750  dff1o6  6751  fliftel  6779  oprabid  6901  mpt22eqb  6995  ralrnmpt2  7001  uniuni  7197  dflim3  7273  dfom2  7293  elxp4  7336  elxp5  7337  opabex3d  7371  opabex3  7372  el2xptp  7439  xporderlem  7518  dfrecs3  7701  tz7.48lem  7768  seqomlem2  7778  oaord  7860  oeeu  7916  nnaord  7932  ecid  8043  mptelixpg  8178  elixpsn  8180  xpsnen  8279  xpcomco  8285  xpassen  8289  omxpenlem  8296  dom0  8323  modom  8396  tz9.12lem3  8895  rankxpsuc  8988  cp  8997  cardprclem  9084  infxpenlem  9115  dfac5lem1  9225  dfac5lem2  9226  dfac5lem5  9229  dfac10c  9241  kmlem3  9255  kmlem12  9264  kmlem13  9265  kmlem14  9266  kmlem15  9267  ackbij2  9346  cflim2  9366  dffin7-2  9501  dfacfin7  9502  fin1a2lem12  9514  axdc3lem3  9555  cfpwsdom  9687  recmulnq  10067  genpass  10112  psslinpr  10134  suplem2pr  10156  opelreal  10232  ltxrlt  10389  addid1  10497  fimaxre  11249  elnn0  11557  elxnn0  11627  elnn0z  11652  nnwos  11970  elxr  12162  xrnepnf  12164  elfzuzb  12555  4fvwrd4  12679  preduz  12681  elfzo2  12693  ssnn0fi  13004  sqeqori  13195  xpcogend  13934  cotr2g  13936  fsumcom2  14724  modfsummod  14744  fprodcom2  14931  rpnnen2lem12  15170  gcdcllem1  15436  isprm2  15609  isprm7  15633  pythagtriplem2  15735  infpn2  15830  4sqlem12  15873  initoid  16855  termoid  16856  eldmcoa  16915  oduposb  17337  gsumwspan  17584  isnsg2  17822  isnsg4  17835  efgcpbllemb  18365  dmdprd  18595  dprdval  18600  dprdw  18607  dprd2d2  18641  dfrhm2  18917  brric2  18945  issubrg  18980  islmim  19265  lbsextlem2  19364  opsrtoslem1  19688  cnfldfunALT  19963  pjfval2  20260  fvmptnn04if  20864  ntreq0  21092  cmpcov2  21404  cmpsub  21414  2ndcdisj  21470  unisngl  21541  txbas  21581  elpt  21586  txkgen  21666  xkococn  21674  fbun  21854  trfil2  21901  fin1aufil  21946  alexsubALTlem3  22063  cnextcn  22081  qustgplem  22134  eltsms  22146  ustn0  22234  fmucndlem  22305  metrest  22539  restmetu  22585  isclmp  23106  srabn  23366  ellogdm  24598  1cubr  24782  leibpilem2  24881  dmarea  24897  vmasum  25154  dchrelbas2  25175  2lgslem4  25344  tgcgr4  25639  ltgov  25705  axlowdimlem13  26047  axeuclidlem  26055  numedglnl  26253  nbgrelOLD  26449  nbupgrres  26480  vtxd0nedgb  26611  rusgrprc  26713  usgr2pth0  26888  wspthsnwspthsnon  27053  isclwwlk  27126  clwwlkn1  27189  clwwlkn2  27192  clwwlknonel  27261  3pthdlem1  27336  iseupthf1o  27374  frgr3v  27449  fusgr2wsp2nb  27508  frgrregord013  27582  h2hcau  28163  h2hlm  28164  axhcompl-zf  28182  shlesb1i  28572  shne0i  28634  chnlei  28671  cmbr2i  28782  pjneli  28909  ho02i  29015  adjsym  29019  adjeu  29075  lnopeqi  29194  largei  29453  atoml2i  29569  cdj3lem3b  29626  or3di  29634  mo5f  29651  rmo3f  29660  rmo4fOLD  29661  disjnf  29708  disjorf  29716  ssrelf  29751  ofpreima  29791  disjdsct  29806  1stpreima  29810  2ndpreima  29811  f1od2  29825  xrdifh  29868  nndiffz1  29874  ordtconnlem1  30294  ind1a  30405  measiuns  30604  elunirnmbfm  30639  eulerpartlemr  30760  eulerpartlemgh  30764  eulerpartlemn  30767  ballotlemodife  30883  bnj250  31091  bnj334  31103  bnj345  31104  bnj89  31111  bnj115  31115  bnj919  31158  bnj1304  31211  bnj92  31253  bnj124  31262  bnj126  31264  bnj154  31269  bnj155  31270  bnj523  31278  bnj526  31279  bnj540  31283  bnj581  31299  bnj916  31324  bnj929  31327  bnj964  31334  bnj978  31340  bnj983  31342  bnj1039  31360  bnj1040  31361  bnj1123  31375  bnj1128  31379  bnj1398  31423  cvmlift2lem1  31605  elmthm  31794  quad3  31884  3orit  31916  brtp  31959  dftr6  31960  dfpo2  31965  eldm3  31971  elrn3  31972  elima4  31997  19.12b  32025  frpoind  32059  frind  32062  nosupbnd1lem4  32176  nosupbnd2lem1  32180  slenlt  32196  madeval2  32255  brtxp  32306  brtxp2  32307  brpprod  32311  brpprod3a  32312  elfix  32329  dffix2  32331  ellimits  32336  dffun10  32340  elfuns  32341  elsingles  32344  brimg  32363  brapply  32364  brsuccf  32367  funpartlem  32368  brrestrict  32375  dfrecs2  32376  dfrdg4  32377  brlb  32381  altopthc  32397  altopthd  32398  fvtransport  32458  hfext  32609  nn0prpw  32637  filnetlem4  32695  df3nandALT2  32714  bj-ssbn  32954  bj-cleljustab  33157  bj-sbeq  33202  bj-csbsnlem  33204  bj-elsngl  33264  bj-eltag  33273  bj-tagex  33283  bj-projun  33290  bj-disj2r  33321  bj-restuni  33359  bj-eldiag  33406  bj-eldiag2  33407  topdifinffinlem  33509  relowlpssretop  33526  phpreu  33704  poimirlem24  33744  poimirlem26  33746  poimirlem30  33750  areacirclem5  33814  isbnd2  33891  sbcalf  34226  sbcexf  34227  sbccom2  34238  sbccom2f  34239  sbccom2fi  34240  csbcom2fi  34242  anan  34318  idinxpssinxp2  34402  ineleq  34430  brabidga  34439  inxpxrn  34464  rnxrn  34467  cossssid2  34529  cossssid3  34530  cosscnvssid3  34537  prtlem70  34633  prtlem16  34646  ishlat2  35131  polval2N  35684  dicelval3  36958  mapdordlem1a  37412  fz1eqin  37831  7rexfrabdioph  37863  rmydioph  38079  dford4  38094  areaquad  38299  ifpan23  38301  ifpdfnan  38328  ifpdfxor  38329  ifpidg  38333  ifpid1g  38336  ifpim123g  38342  ifp1bi  38344  ifpimimb  38346  ifpororb  38347  ifpbibib  38352  rp-fakenanass  38357  rp-fakeuninass  38359  cllem0  38368  rababg  38376  elmapintrab  38379  elmapintab  38399  undmrnresiss  38407  ss2iundf  38448  dfxor4  38555  rp-imass  38562  dfhe3  38566  dffrege115  38769  frege131  38785  frege133  38787  clsk1indlem4  38839  clsk1indlem1  38840  undisjrab  39002  pm13.196a  39111  eelT11  39427  eelTT1  39430  eelT01  39431  eel0T1  39432  uunTT1  39514  uunTT1p1  39515  uunTT1p2  39516  uunT11  39517  uunT11p1  39518  uunT11p2  39519  uun111  39526  iunssf  39753  ssrabf  39787  rabssf  39791  disjinfi  39866  elicores  40237  fourierdlem42  40842  iundjiun  41153  2reu7  41700  2reu8  41701  dfdfat2  41714  aovov0bi  41782  afv2orxorb  41814  afv2ndeffv0  41846  257prm  42045  fmtno4prmfac  42056  nnsum4primeseven  42260  nnsum4primesevenALTV  42261  uspgrsprf1  42320  opeliun2xp  42676  aacllem  43115