Theorem 3bitri 299

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  bibi1i  341  pm5.32  576  biadan  817  orbi1i  910  orass  918  or32  922  cases  1037  3anidm  1100  an3andi  1478  an33rean  1479  an33reanOLD  1480  nanbi  1490  excxor  1507  norassOLD  1534  cadan  1610  cadcomb  1614  nic-axALT  1675  tbw-bijust  1699  rb-bijust  1750  nf2  1786  19.43  1883  19.43OLD  1884  3exdistr  1962  19.12vvv  1995  sb3an  2087  equsb3rOLD  2111  sbcom2  2168  excom13  2171  sbco4  2284  sbn  2287  19.12vv  2368  eeeanv  2371  ee4anv  2372  2sb8ev  2375  sbel2x  2498  sbnOLD  2541  2sb8e  2576  sbnALT  2595  dfmo  2682  sb8eulem  2684  2mo2  2732  2eu7  2743  2eu8  2744  r19.26-3  3172  r19.23v  3279  rexcom  3355  ralcom13  3359  rexcom13  3360  cbvreuw  3443  cbvreu  3447  ceqsralt  3528  ceqsex2  3543  ceqsex2v  3544  ceqsex4v  3546  ralrab2  3690  rexrab2  3693  reu2  3716  rmo4  3721  reu8  3724  rmo3f  3725  2reu5lem3  3748  sbc3an  3838  reu8nf  3860  rmo2  3870  rmo3  3872  rmo3OLD  3873  rmoanim  3878  dfss2  3955  ss2rab  4047  rabss  4048  ssrab  4049  dfdif3  4091  symdifass  4228  dfss4  4235  undi  4251  undif3  4265  difin2  4266  dfnul2OLD  4294  difin0ss  4328  disj  4399  disj4  4408  rabsssn  4607  disjsn  4647  raldifsni  4728  ssunpr  4765  sspr  4766  sstp  4767  uni0b  4864  uni0c  4865  ssint  4892  iunss  4969  iundif2  4996  disjor  5046  nfnid  5276  reusv2lem4  5302  ssextss  5346  exss  5355  eqvinop  5378  sbcop  5380  opcom  5391  opeqpr  5395  brabsb  5418  opelopabf  5432  dfid3  5462  pofun  5491  opeliunxp  5619  xpiundi  5622  brinxp2  5629  reliun  5689  exopxfr  5714  cnvuni  5757  dmopab3  5788  rnep  5797  elres  5891  elsnres  5892  elrid  5913  asymref2  5977  intirr  5978  xpeq0  6017  xpdifid  6025  ssrnres  6035  dminxp  6037  dfrel4v  6047  elid  6056  dmsnn0  6064  rnco  6105  coeq0  6108  sspred  6156  wfi  6181  sb8iota  6325  dffun2  6365  fun11  6428  isarep1  6442  dff1o4  6623  opabiota  6746  fvopab5  6800  eqfnfv3  6804  fvn0ssdmfun  6842  fnressn  6920  f13dfv  7031  dff1o6  7032  fliftel  7062  oprabidw  7187  oprabid  7188  mpo2eqb  7283  ralrnmpo  7289  uniuni  7484  dflim3  7562  dfom2  7582  elxp4  7627  elxp5  7628  opabex3d  7666  opabex3rd  7667  opabex3  7668  el2xptp  7735  fsplit  7812  xporderlem  7821  dfrecs3  8009  tz7.48lem  8077  seqomlem2  8087  oaord  8173  oeeu  8229  nnaord  8245  ecid  8362  mptelixpg  8499  elixpsn  8501  xpsnen  8601  xpcomco  8607  xpassen  8611  omxpenlem  8618  dom0  8645  modom  8719  tz9.12lem3  9218  rankxpsuc  9311  cp  9320  cardprclem  9408  infxpenlem  9439  dfac5lem1  9549  dfac5lem2  9550  dfac5lem5  9553  dfac10c  9564  kmlem3  9578  kmlem12  9587  kmlem13  9588  kmlem14  9589  kmlem15  9590  ackbij2  9665  cf0  9673  cflim2  9685  dffin7-2  9820  dfacfin7  9821  fin1a2lem12  9833  axdc3lem3  9874  cfpwsdom  10006  recmulnq  10386  genpass  10431  psslinpr  10453  suplem2pr  10475  opelreal  10552  ltxrlt  10711  addid1  10820  fimaxreOLD  11585  elnn0  11900  elxnn0  11970  elnn0z  11995  nnwos  12316  elxr  12512  xrnepnf  12514  elfzuzb  12903  4fvwrd4  13028  preduz  13030  elfzo2  13042  ssnn0fi  13354  sqeqori  13577  xpcogend  14334  cotr2g  14336  fsumcom2  15129  modfsummod  15149  fprodcom2  15338  rpnnen2lem12  15578  gcdcllem1  15848  isprm2  16026  isprm7  16052  pythagtriplem2  16154  infpn2  16249  4sqlem12  16292  initoid  17265  termoid  17266  eldmcoa  17325  oduposb  17746  gsumwspan  18011  smndex1basss  18070  smndex1mgm  18072  isnsg2  18308  isnsg4  18319  cycsubmel  18343  efgcpbllemb  18881  dmdprd  19120  dprdval  19125  dprdw  19132  dprd2d2  19166  dfrhm2  19469  brric2  19500  issubrg  19535  islmim  19834  lbsextlem2  19931  opsrtoslem1  20264  cnfldfunALT  20558  pjfval2  20853  ntreq0  21685  cmpcov2  21998  cmpsub  22008  2ndcdisj  22064  unisngl  22135  txbas  22175  elpt  22180  txkgen  22260  xkococn  22268  fbun  22448  trfil2  22495  fin1aufil  22540  alexsubALTlem3  22657  cnextcn  22675  qustgplem  22729  eltsms  22741  ustn0  22829  fmucndlem  22900  metrest  23134  restmetu  23180  isclmp  23701  srabn  23963  ellogdm  25222  1cubr  25420  leibpilem2  25519  dmarea  25535  vmasum  25792  dchrelbas2  25813  2lgslem4  25982  tgcgr4  26317  ltgov  26383  axlowdimlem13  26740  axeuclidlem  26748  numedglnl  26929  nbupgrres  27146  vtxd0nedgb  27270  rusgrprc  27372  usgr2pth0  27546  wspthsnwspthsnon  27695  isclwwlk  27762  clwwlkn1  27819  clwwlkn2  27822  clwwlknonel  27874  3pthdlem1  27943  iseupthf1o  27981  frgr3v  28054  fusgr2wsp2nb  28113  frgrregord013  28174  h2hcau  28756  h2hlm  28757  shlesb1i  29163  shne0i  29225  chnlei  29262  cmbr2i  29373  pjneli  29500  ho02i  29606  adjsym  29610  adjeu  29666  lnopeqi  29785  largei  30044  atoml2i  30160  cdj3lem3b  30217  or3di  30225  mo5f  30253  dmrab  30260  disjnf  30320  disjorf  30329  ssrelf  30366  ofpreima  30410  disjdsct  30438  1stpreima  30442  2ndpreima  30443  f1od2  30457  xrdifh  30503  nndiffz1  30509  ordtconnlem1  31167  ind1a  31278  measiuns  31476  elunirnmbfm  31511  eulerpartlemr  31632  eulerpartlemgh  31636  eulerpartlemn  31639  ballotlemodife  31755  bnj250  31971  bnj334  31983  bnj345  31984  bnj89  31991  bnj115  31995  bnj919  32038  bnj1304  32091  bnj92  32134  bnj124  32143  bnj126  32145  bnj154  32150  bnj155  32151  bnj523  32159  bnj526  32160  bnj540  32164  bnj581  32180  bnj916  32205  bnj929  32208  bnj964  32215  bnj978  32221  bnj983  32223  bnj1039  32243  bnj1040  32244  bnj1123  32258  bnj1128  32262  bnj1398  32306  lfuhgr3  32366  cvmlift2lem1  32549  satfv0  32605  satf0  32619  satf0op  32624  satffunlem  32648  satffunlem1lem1  32649  satffunlem2lem1  32651  elmthm  32823  quad3  32913  3orit  32945  brtp  32985  dftr6  32986  dfpo2  32991  eldm3  32997  elrn3  32998  elima4  33019  19.12b  33046  frpoind  33080  frind  33085  nosupbnd1lem4  33211  nosupbnd2lem1  33215  slenlt  33231  madeval2  33290  brtxp  33341  brtxp2  33342  brpprod  33346  brpprod3a  33347  elfix  33364  dffix2  33366  ellimits  33371  sscoid  33374  dffun10  33375  elfuns  33376  elsingles  33379  brimg  33398  brapply  33399  brsuccf  33402  funpartlem  33403  brrestrict  33410  dfrecs2  33411  dfrdg4  33412  brlb  33416  altopthc  33432  altopthd  33433  fvtransport  33493  hfext  33644  nn0prpw  33671  filnetlem4  33729  df3nandALT2  33748  bj-sbeq  34221  bj-csbsnlem  34223  bj-elsngl  34283  bj-eltag  34292  bj-tagex  34302  bj-projun  34309  bj-reabeq  34342  bj-disj2r  34343  bj-restuni  34391  bj-elid6  34465  bj-eldiag  34471  bj-eldiag2  34472  topdifinffinlem  34631  relowlpssretop  34648  fvineqsneq  34696  wl-dfclab  34843  wl-dfrexsb  34866  phpreu  34891  poimirlem24  34931  poimirlem26  34933  poimirlem30  34937  areacirclem5  35001  isbnd2  35076  sbcalf  35407  sbcexf  35408  sbccom2  35418  sbccom2f  35419  sbccom2fi  35420  csbcom2fi  35421  anan  35514  idinxpssinxp2  35590  ineleq  35623  brabidgaw  35632  brabidga  35633  inxpxrn  35658  rnxrn  35661  cossssid2  35723  cossssid3  35724  cosscnvssid3  35731  dfeldisj3  35967  dfeldisj4  35968  prtlem70  36008  prtlem16  36020  ishlat2  36504  pmapglb  36921  polval2N  37057  dicelval3  38331  mapdordlem1a  38785  prjspeclsp  39311  fz1eqin  39415  7rexfrabdioph  39446  rmydioph  39660  dford4  39675  areaquad  39872  ifpan23  39874  ifpdfnan  39901  ifpdfxor  39902  ifpidg  39906  ifpid1g  39909  ifpim123g  39915  ifp1bi  39917  ifpimimb  39919  ifpororb  39920  ifpbibib  39925  rp-fakeuninass  39931  dfsucon  39938  cllem0  39974  rababg  39982  elmapintrab  39985  elmapintab  40005  undmrnresiss  40013  ss2iundf  40053  dfxor4  40160  rp-imass  40166  dfhe3  40170  dffrege115  40373  frege131  40389  frege133  40391  clsk1indlem4  40443  clsk1indlem1  40444  expandrexn  40676  rr-groth  40684  undisjrab  40687  pm13.196a  40795  eelT11  41090  eelTT1  41093  eelT01  41094  eel0T1  41095  uunTT1  41176  uunTT1p1  41177  uunTT1p2  41178  uunT11  41179  uunT11p1  41180  uunT11p2  41181  uun111  41188  iunssf  41401  ssrabf  41430  rabssf  41434  disjinfi  41503  elicores  41858  fourierdlem42  42483  iundjiun  42791  2reu7  43359  2reu8  43360  2reu8i  43361  dfdfat2  43376  aovov0bi  43444  afv2orxorb  43476  afv2ndeffv0  43508  ichcircshi  43661  icheq  43669  ichal  43676  prpair  43712  prproropf1olem0  43713  257prm  43772  fmtno4prmfac  43783  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  uspgrsprf1  44071  opeliun2xp  44430  rrx2xpref1o  44754  aacllem  44951