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  912  orass  920  or32  924  cases  1043  dn1  1058  3anidm  1104  an33rean  1483  nanbi  1497  excxor  1513  cadan  1606  cadcomb  1610  nic-axALT  1672  tbw-bijust  1696  rb-bijust  1747  nf2  1783  19.43  1881  19.43OLD  1882  3exdistr  1960  19.12vvv  1988  excom13  2165  sbcom2  2174  sbco4OLD  2176  sbn  2284  sbnf  2316  19.12vv  2353  eeeanv  2356  ee4anv  2357  2sb8ef  2362  sbel2x  2482  2sb8e  2538  dfmo  2599  sb8eulem  2601  2mo2  2650  2eu7  2661  2eu8  2662  sbabel  2944  r19.23v  3189  2ralor  3237  rexcomOLD  3297  ralcom13OLD  3301  rexcom13  3302  cbvreuwOLD  3423  cbvreu  3435  rabrabi  3463  cgsex4g  3538  ceqsex2  3547  ceqsex2v  3548  ceqsex3v  3549  ceqsex4v  3550  ceqsex6v  3551  ceqsex8v  3552  ralrab2  3720  rexrab2  3722  reu2  3747  rmo4  3752  reu8  3755  rmo3f  3756  2reu5lem3  3779  sbcimdv  3878  reu8nf  3899  rmo2  3909  rmo3  3911  rmoanim  3916  ss2rab  4094  rabss  4095  ssrab  4096  dfdif3OLD  4141  symdifass  4281  dfss4  4288  undi  4304  indifdi  4313  undif3  4319  reuun2  4344  difin0ss  4396  ab0OLD  4403  disj  4473  disj4  4482  rabsssn  4690  disjsn  4736  snssb  4807  raldifsni  4820  ssunpr  4859  sspr  4860  sstp  4861  uni0b  4957  uni0c  4958  ssint  4988  intprg  5005  iunssf  5067  iunss  5068  iundif2  5097  disjor  5148  nfnid  5393  reusv2lem4  5419  ssextss  5473  exss  5483  eqvinop  5507  sbcop  5509  opcom  5520  opeqpr  5524  brtp  5542  brabsb  5550  opelopabf  5564  dfid3  5596  pofun  5626  opeliunxp  5767  xpiundi  5770  brinxp2  5777  reliun  5840  exopxfr  5868  cnvuni  5911  dmopab3  5944  rnep  5951  dmxp  5953  elres  6049  elsnres  6050  elrid  6075  cnvsym  6144  cnvsymOLD  6145  asymref2  6149  intirr  6150  cnvopab  6169  xpeq0  6191  difxp  6195  xpdifid  6199  ssrnres  6209  dminxp  6211  dfrel4v  6221  elid  6230  dmsnn0  6238  imaco  6282  rnco  6283  coeq0  6286  resssxp  6301  dfpo2  6327  snres0  6329  sspred  6341  frpoind  6374  wfiOLD  6383  sb8iota  6537  dffun2OLDOLD  6585  fun11  6652  isarep1  6667  isarep1OLD  6668  dff1o4  6870  opabiota  7004  fvopab5  7062  eqfnfv3  7066  fvn0ssdmfun  7108  fnressn  7192  f13dfv  7310  dff1o6  7311  fliftel  7345  oprabidw  7479  oprabid  7480  eloprabga  7558  mpo2eqb  7582  ralrnmpo  7589  uniuni  7797  dflim3  7884  dfom2  7905  elxp4  7962  elxp5  7963  opabex3d  8006  opabex3rd  8007  opabex3  8008  el2xptp  8076  fsplit  8158  xporderlem  8168  ralxp3f  8178  frpoins3xpg  8181  poxp2  8184  suppvalbr  8205  dfrecs3  8428  dfrecs3OLD  8429  tz7.48lem  8497  seqomlem2  8507  oaord  8603  oeeu  8659  nnaord  8675  ecid  8840  mptelixpg  8993  elixpsn  8995  xpsnen  9121  xpcomco  9128  xpassen  9132  omxpenlem  9139  dom0OLD  9169  modom  9307  brttrcl2  9783  ttrcltr  9785  rnttrcl  9791  frind  9819  tz9.12lem3  9858  rankxpsuc  9951  cp  9960  cardprclem  10048  infxpenlem  10082  dfac5lem1  10192  dfac5lem2  10193  dfac5lem5  10196  dfac10c  10208  kmlem3  10222  kmlem12  10231  kmlem13  10232  kmlem14  10233  kmlem15  10234  ackbij2  10311  cf0  10320  cflim2  10332  dffin7-2  10467  dfacfin7  10468  fin1a2lem12  10480  axdc3lem3  10521  cfpwsdom  10653  recmulnq  11033  genpass  11078  psslinpr  11100  suplem2pr  11122  opelreal  11199  ltxrlt  11360  addrid  11470  elnn0  12555  elxnn0  12627  elnn0z  12652  nnwos  12980  elxr  13179  xrnepnf  13181  elfzuzb  13578  4fvwrd4  13705  preduz  13707  elfzo2  13719  ssnn0fi  14036  sqeqori  14263  xpcogend  15023  cotr2g  15025  fsumcom2  15822  modfsummod  15842  fprodcom2  16032  rpnnen2lem12  16273  gcdcllem1  16545  isprm2  16729  isprm7  16755  pythagtriplem2  16864  infpn2  16960  4sqlem12  17003  initoid  18068  termoid  18069  eldmcoa  18132  oduposb  18399  gsumwspan  18881  smndex1basss  18940  smndex1mgm  18942  isnsg2  19196  isnsg4  19207  cycsubmel  19240  efgcpbllemb  19797  dmdprd  20042  dprdval  20047  dprdw  20054  dprd2d2  20088  dfrhm2  20500  brric2  20532  issubrg  20599  isdomn5  20732  islmim  21084  lbsextlem2  21184  cnfldfun  21401  cnfldfunOLD  21414  pzriprnglem3  21517  pjfval2  21752  opsrtoslem1  22102  ntreq0  23106  cmpcov2  23419  cmpsub  23429  2ndcdisj  23485  unisngl  23556  txbas  23596  elpt  23601  txkgen  23681  xkococn  23689  fbun  23869  trfil2  23916  fin1aufil  23961  alexsubALTlem3  24078  cnextcn  24096  qustgplem  24150  eltsms  24162  ustn0  24250  fmucndlem  24321  metrest  24558  restmetu  24604  isclmp  25149  srabn  25413  ellogdm  26699  1cubr  26903  leibpilem2  27002  dmarea  27018  vmasum  27278  dchrelbas2  27299  2lgslem4  27468  nosupbnd1lem4  27774  nosupbnd2lem1  27778  slenlt  27815  madeval2  27910  made0  27930  tgcgr4  28557  ltgov  28623  axlowdimlem13  28987  axeuclidlem  28995  numedglnl  29179  nbupgrres  29399  vtxd0nedgb  29524  rusgrprc  29626  usgr2pth0  29801  wspthsnwspthsnon  29949  isclwwlk  30016  clwwlkn1  30073  clwwlkn2  30076  clwwlknonel  30127  3pthdlem1  30196  iseupthf1o  30234  frgr3v  30307  fusgr2wsp2nb  30366  frgrregord013  30427  h2hcau  31011  h2hlm  31012  shlesb1i  31418  shne0i  31480  chnlei  31517  cmbr2i  31628  pjneli  31755  ho02i  31861  adjsym  31865  adjeu  31921  lnopeqi  32040  largei  32299  atoml2i  32415  cdj3lem3b  32472  or3di  32488  mo5f  32517  dmrab  32525  rabsspr  32529  rabsstp  32530  disjnf  32592  disjorf  32601  ssrelf  32637  ofpreima  32683  disjdsct  32714  1stpreima  32718  2ndpreima  32719  f1od2  32735  xrdifh  32785  nndiffz1  32791  prmidl0  33443  zarclsun  33816  ordtconnlem1  33870  ind1a  33983  measiuns  34181  elunirnmbfm  34216  eulerpartlemr  34339  eulerpartlemgh  34343  eulerpartlemn  34346  ballotlemodife  34462  bnj250  34677  bnj334  34689  bnj345  34690  bnj89  34697  bnj115  34701  bnj919  34743  bnj1304  34795  bnj92  34838  bnj124  34847  bnj126  34849  bnj154  34854  bnj155  34855  bnj523  34863  bnj526  34864  bnj540  34868  bnj581  34884  bnj916  34909  bnj929  34912  bnj964  34919  bnj978  34925  bnj983  34927  bnj1039  34947  bnj1040  34948  bnj1123  34962  bnj1128  34966  bnj1398  35010  lfuhgr3  35087  cvmlift2lem1  35270  satfv0  35326  satf0  35340  satf0op  35345  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  elmthm  35544  quad3  35638  3orit  35678  dftr6  35713  eldm3  35723  elrn3  35724  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  36191  nn0prpw  36289  filnetlem4  36347  df3nandALT2  36366  bj-sbeq  36867  bj-csbsnlem  36869  bj-elsngl  36934  bj-eltag  36943  bj-tagex  36953  bj-projun  36960  bj-reabeq  36993  bj-disj2r  36994  bj-restuni  37063  bj-elid6  37136  bj-eldiag  37142  bj-eldiag2  37143  topdifinffinlem  37313  relowlpssretop  37330  fvineqsneq  37378  wl-3xorbi  37439  wl-2mintru1  37456  wl-df3maxtru1  37458  wl-dfclab  37550  phpreu  37564  poimirlem24  37604  poimirlem26  37606  poimirlem30  37610  areacirclem5  37672  isbnd2  37743  sbcalf  38074  sbcexf  38075  sbccom2  38085  sbccom2f  38086  sbccom2fi  38087  csbcom2fi  38088  anan  38183  br1cnvinxp  38212  idinxpssinxp2  38274  ineleq  38310  brabidgaw  38321  brabidga  38322  inxpxrn  38351  rnxrn  38354  cossssid2  38424  cossssid3  38425  cosscnvssid3  38432  dfeldisj3  38675  dfeldisj4  38676  antisymrelres  38719  dfmembpart2  38726  mpet3  38792  cpet2  38793  prtlem70  38813  prtlem16  38825  ishlat2  39309  pmapglb  39727  polval2N  39863  dicelval3  41137  mapdordlem1a  41591  fimgmcyclem  42488  fimgmcyc  42489  prjspeclsp  42567  sn-isghm  42628  abbibw  42632  fz1eqin  42725  7rexfrabdioph  42756  rmydioph  42971  dford4  42986  areaquad  43177  onsupmaxb  43200  onov0suclim  43236  nnoeomeqom  43274  tfsconcat0i  43307  faosnf0.11b  43389  ifpan23  43422  ifpdfnan  43448  ifpdfxor  43449  ifpidg  43453  ifpid1g  43456  ifpim123g  43462  ifp1bi  43464  ifpimimb  43466  ifpororb  43467  ifpbibib  43472  rp-fakeuninass  43478  dfsucon  43485  minregex  43496  cllem0  43528  rababg  43536  elmapintrab  43538  elmapintab  43558  undmrnresiss  43566  dfxor4  43728  dfhe3  43737  dffrege115  43940  frege131  43956  frege133  43958  clsk1indlem4  44006  clsk1indlem1  44007  expandrexn  44260  rr-groth  44268  rr-grothshortbi  44272  undisjrab  44275  pm13.196a  44383  eelT11  44678  eelTT1  44681  eelT01  44682  eel0T1  44683  uunTT1  44764  uunTT1p1  44765  uunTT1p2  44766  uunT11  44767  uunT11p1  44768  uunT11p2  44769  uun111  44776  xpwf  44912  ssrabf  45016  rabssf  45021  disjinfi  45099  elicores  45451  fourierdlem42  46070  iundjiun  46381  2reu7  47026  2reu8  47027  2reu8i  47028  dfdfat2  47043  aovov0bi  47111  afv2orxorb  47143  afv2ndeffv0  47175  ichcircshi  47328  ichan  47329  icheq  47336  ichal  47340  prpair  47375  prproropf1olem0  47376  257prm  47435  fmtno4prmfac  47446  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  clnbgrel  47701  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  uspgrsprf1  47870  opeliun2xp  48057  rrx2xpref1o  48452  isthincd2  48705  aacllem  48895