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  3102  r19.23v  3161  2ralor  3211  ralcom13OLD  3270  rexcom13  3271  cbvreu  3397  rabrabi  3425  cgsex4g  3494  ceqsex2  3501  ceqsex2v  3502  ceqsex3v  3503  ceqsex4v  3504  ceqsex6v  3505  ceqsex8v  3506  ralrab2  3669  rexrab2  3671  reu2  3696  rmo4  3701  reu8  3704  rmo3f  3705  2reu5lem3  3728  sbcimdv  3822  reu8nf  3840  rmo2  3850  rmo3  3852  rmoanim  3857  ss2rab  4034  rabss  4035  ssrab  4036  dfdif3OLD  4081  symdifass  4225  dfss4  4232  undi  4248  indifdi  4257  undif3  4263  reuun2  4288  difin0ss  4336  disj  4413  disj4  4422  rabsssn  4632  disjsn  4675  snssb  4746  raldifsni  4759  ssunpr  4798  sspr  4799  sstp  4800  uni0b  4897  uni0c  4898  ssint  4928  intprg  4945  iunssf  5008  iunss  5009  iundif2  5038  disjor  5089  nfnid  5330  reusv2lem4  5356  ssextss  5413  exss  5423  eqvinop  5447  sbcop  5449  opcom  5461  opeqpr  5465  brtp  5483  brabsb  5491  opelopabf  5505  dfid3  5536  pofun  5564  opeliunxp  5705  opeliun2xp  5706  xpiundi  5709  brinxp2  5716  reliun  5779  exopxfr  5807  cnvuni  5850  dmopab3  5883  rnep  5890  dmxp  5892  rnopab3  5920  elres  5991  elsnres  5992  elrid  6017  cnvsym  6085  cnvsymOLD  6086  asymref2  6090  intirr  6091  cnvopab  6110  xpeq0  6133  difxp  6137  xpdifid  6141  ssrnres  6151  dminxp  6153  dfrel4v  6163  elid  6172  dmsnn0  6180  imaco  6224  rnco  6225  coeq0  6228  resssxp  6243  dfpo2  6269  snres0  6271  sspred  6283  frpoind  6315  sb8iota  6475  dffun2OLDOLD  6523  fun11  6590  isarep1  6606  isarep1OLD  6607  dff1o4  6808  opabiota  6943  fvopab5  7001  eqfnfv3  7005  fvn0ssdmfun  7046  fnressn  7130  f13dfv  7249  dff1o6  7250  fliftel  7284  oprabidw  7418  oprabid  7419  eloprabga  7498  mpo2eqb  7521  ralrnmpo  7528  uniuni  7738  dflim3  7823  dfom2  7844  elxp4  7898  elxp5  7899  opabex3d  7944  opabex3rd  7945  opabex3  7946  el2xptp  8014  fsplit  8096  xporderlem  8106  ralxp3f  8116  frpoins3xpg  8119  poxp2  8122  suppvalbr  8143  dfrecs3  8341  tz7.48lem  8409  seqomlem2  8419  oaord  8511  oeeu  8567  nnaord  8583  ecid  8753  mptelixpg  8908  elixpsn  8910  xpsnen  9025  xpcomco  9031  xpassen  9035  omxpenlem  9042  modom  9191  brttrcl2  9667  ttrcltr  9669  rnttrcl  9675  frind  9703  tz9.12lem3  9742  rankxpsuc  9835  cp  9844  cardprclem  9932  infxpenlem  9966  dfac5lem1  10076  dfac5lem2  10077  dfac5lem5  10080  dfac10c  10092  kmlem3  10106  kmlem12  10115  kmlem13  10116  kmlem14  10117  kmlem15  10118  ackbij2  10195  cf0  10204  cflim2  10216  dffin7-2  10351  dfacfin7  10352  fin1a2lem12  10364  axdc3lem3  10405  cfpwsdom  10537  recmulnq  10917  genpass  10962  psslinpr  10984  suplem2pr  11006  opelreal  11083  ltxrlt  11244  addrid  11354  elnn0  12444  elxnn0  12517  elnn0z  12542  nnwos  12874  elxr  13076  xrnepnf  13078  elfzuzb  13479  4fvwrd4  13609  preduz  13611  elfzo2  13623  ssnn0fi  13950  sqeqori  14179  xpcogend  14940  cotr2g  14942  fsumcom2  15740  modfsummod  15760  fprodcom2  15950  rpnnen2lem12  16193  gcdcllem1  16469  isprm2  16652  isprm7  16678  pythagtriplem2  16788  infpn2  16884  4sqlem12  16927  initoid  17963  termoid  17964  eldmcoa  18027  oduposb  18288  gsumwspan  18773  smndex1basss  18832  smndex1mgm  18834  isnsg2  19088  isnsg4  19099  cycsubmel  19132  efgcpbllemb  19685  dmdprd  19930  dprdval  19935  dprdw  19942  dprd2d2  19976  dfrhm2  20383  brric2  20415  issubrg  20480  isdomn5  20619  islmim  20969  lbsextlem2  21069  cnfldfun  21278  cnfldfunOLD  21291  pzriprnglem3  21393  pjfval2  21618  opsrtoslem1  21962  ntreq0  22964  cmpcov2  23277  cmpsub  23287  2ndcdisj  23343  unisngl  23414  txbas  23454  elpt  23459  txkgen  23539  xkococn  23547  fbun  23727  trfil2  23774  fin1aufil  23819  alexsubALTlem3  23936  cnextcn  23954  qustgplem  24008  eltsms  24020  ustn0  24108  fmucndlem  24178  metrest  24412  restmetu  24458  isclmp  24997  srabn  25260  ellogdm  26548  1cubr  26752  leibpilem2  26851  dmarea  26867  vmasum  27127  dchrelbas2  27148  2lgslem4  27317  nosupbnd1lem4  27623  nosupbnd2lem1  27627  slenlt  27664  madeval2  27761  made0  27785  onsiso  28169  onsfi  28247  tgcgr4  28458  ltgov  28524  axlowdimlem13  28881  axeuclidlem  28889  numedglnl  29071  nbupgrres  29291  vtxd0nedgb  29416  rusgrprc  29518  usgr2pth0  29695  wspthsnwspthsnon  29846  isclwwlk  29913  clwwlkn1  29970  clwwlkn2  29973  clwwlknonel  30024  3pthdlem1  30093  iseupthf1o  30131  frgr3v  30204  fusgr2wsp2nb  30263  frgrregord013  30324  h2hcau  30908  h2hlm  30909  shlesb1i  31315  shne0i  31377  chnlei  31414  cmbr2i  31525  pjneli  31652  ho02i  31758  adjsym  31762  adjeu  31818  lnopeqi  31937  largei  32196  atoml2i  32312  cdj3lem3b  32369  or3di  32388  mo5f  32418  dmrab  32426  rabsspr  32430  rabsstp  32431  disjnf  32499  disjorf  32508  ssrelf  32543  ofpreima  32589  disjdsct  32626  1stpreima  32630  2ndpreima  32631  f1od2  32644  xrdifh  32703  nndiffz1  32709  ind1a  32782  prmidl0  33421  zarclsun  33860  ordtconnlem1  33914  measiuns  34207  elunirnmbfm  34242  eulerpartlemr  34365  eulerpartlemgh  34369  eulerpartlemn  34372  ballotlemodife  34489  bnj250  34691  bnj334  34703  bnj345  34704  bnj89  34711  bnj115  34715  bnj919  34757  bnj1304  34809  bnj92  34852  bnj124  34861  bnj126  34863  bnj154  34868  bnj155  34869  bnj523  34877  bnj526  34878  bnj540  34882  bnj581  34898  bnj916  34923  bnj929  34926  bnj964  34933  bnj978  34939  bnj983  34941  bnj1039  34961  bnj1040  34962  bnj1123  34976  bnj1128  34980  bnj1398  35024  lfuhgr3  35107  cvmlift2lem1  35289  satfv0  35345  satf0  35359  satf0op  35364  satffunlem  35388  satffunlem1lem1  35389  satffunlem2lem1  35391  elmthm  35563  quad3  35657  3orit  35703  dftr6  35738  eldm3  35748  elrn3  35749  elima4  35763  19.12b  35789  brtxp  35868  brtxp2  35869  brpprod  35873  brpprod3a  35874  elfix  35891  dffix2  35893  ellimits  35898  sscoid  35901  dffun10  35902  elfuns  35903  elsingles  35906  brimg  35925  brapply  35926  brsuccf  35929  funpartlem  35930  brrestrict  35937  dfrecs2  35938  dfrdg4  35939  brlb  35943  altopthc  35959  altopthd  35960  fvtransport  36020  hfext  36171  ss-ax8  36213  nn0prpw  36311  filnetlem4  36369  df3nandALT2  36388  bj-sbeq  36889  bj-csbsnlem  36891  bj-elsngl  36956  bj-eltag  36965  bj-tagex  36975  bj-projun  36982  bj-reabeq  37015  bj-disj2r  37016  bj-restuni  37085  bj-elid6  37158  bj-eldiag  37164  bj-eldiag2  37165  topdifinffinlem  37335  relowlpssretop  37352  fvineqsneq  37400  wl-3xorbi  37461  wl-2mintru1  37478  wl-df3maxtru1  37480  wl-dfclab  37584  phpreu  37598  poimirlem24  37638  poimirlem26  37640  poimirlem30  37644  areacirclem5  37706  isbnd2  37777  sbcalf  38108  sbcexf  38109  sbccom2  38119  sbccom2f  38120  sbccom2fi  38121  csbcom2fi  38122  anan  38217  br1cnvinxp  38245  idinxpssinxp2  38306  ineleq  38336  brabidgaw  38347  brabidga  38348  inxpxrn  38381  rnxrn  38384  cossssid2  38459  cossssid3  38460  cosscnvssid3  38467  dfeldisj3  38711  dfeldisj4  38712  antisymrelres  38755  dfmembpart2  38762  mpet3  38828  cpet2  38829  prtlem70  38850  prtlem16  38862  ishlat2  39346  pmapglb  39764  polval2N  39900  dicelval3  41174  mapdordlem1a  41628  redvmptabs  42348  fimgmcyclem  42521  fimgmcyc  42522  prjspeclsp  42600  sn-isghm  42661  abbibw  42665  fz1eqin  42757  7rexfrabdioph  42788  rmydioph  43003  dford4  43018  areaquad  43205  onsupmaxb  43228  onov0suclim  43263  nnoeomeqom  43301  tfsconcat0i  43334  faosnf0.11b  43416  ifpan23  43449  ifpdfnan  43475  ifpdfxor  43476  ifpidg  43480  ifpid1g  43483  ifpim123g  43489  ifp1bi  43491  ifpimimb  43493  ifpororb  43494  ifpbibib  43499  rp-fakeuninass  43505  dfsucon  43512  minregex  43523  cllem0  43555  rababg  43563  elmapintrab  43565  elmapintab  43585  undmrnresiss  43593  dfxor4  43755  dfhe3  43764  dffrege115  43967  frege131  43983  frege133  43985  clsk1indlem4  44033  clsk1indlem1  44034  expandrexn  44280  rr-groth  44288  rr-grothshortbi  44292  undisjrab  44295  pm13.196a  44403  eelT11  44696  eelTT1  44699  eelT01  44700  eel0T1  44701  uunTT1  44782  uunTT1p1  44783  uunTT1p2  44784  uunT11  44785  uunT11p1  44786  uunT11p2  44787  uun111  44794  xpwf  44954  permaxinf2lem  45002  permac8prim  45004  ssrabf  45108  rabssf  45113  disjinfi  45186  elicores  45531  fourierdlem42  46147  iundjiun  46458  2reu7  47112  2reu8  47113  2reu8i  47114  dfdfat2  47129  aovov0bi  47197  afv2orxorb  47229  afv2ndeffv0  47261  ichcircshi  47455  ichan  47456  icheq  47463  ichal  47467  prpair  47502  prproropf1olem0  47503  257prm  47562  fmtno4prmfac  47573  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  clnbgrel  47829  isubgr3stgrlem4  47968  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  gpgprismgr4cycllem10  48094  uspgrsprf1  48135  rrx2xpref1o  48707  iinxp  48819  resinsn  48860  resinsnALT  48861  0funcALT  49077  catcsect  49387  isthincd2  49426  aacllem  49790