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  819  orbi1i  914  orass  922  or32  926  cases  1043  dn1  1058  3anidm  1104  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  1988  excom13  2164  sbcom2  2173  sbco4OLD  2175  sbn  2280  sbnf  2312  19.12vv  2349  eeeanv  2352  ee4anv  2353  ee4anvOLD  2354  2sb8ef  2359  sbel2x  2479  2sb8e  2535  dfmo  2596  sb8eulem  2598  2mo2  2647  2eu7  2658  2eu8  2659  sbabel  2938  r19.23v  3183  2ralor  3231  rexcomOLD  3291  ralcom13OLD  3295  rexcom13  3296  cbvreuwOLD  3415  cbvreu  3428  rabrabi  3456  cgsex4g  3528  ceqsex2  3535  ceqsex2v  3536  ceqsex3v  3537  ceqsex4v  3538  ceqsex6v  3539  ceqsex8v  3540  ralrab2  3704  rexrab2  3706  reu2  3731  rmo4  3736  reu8  3739  rmo3f  3740  2reu5lem3  3763  sbcimdv  3859  reu8nf  3877  rmo2  3887  rmo3  3889  rmoanim  3894  ss2rab  4071  rabss  4072  ssrab  4073  dfdif3OLD  4118  symdifass  4262  dfss4  4269  undi  4285  indifdi  4294  undif3  4300  reuun2  4325  difin0ss  4373  disj  4450  disj4  4459  rabsssn  4668  disjsn  4711  snssb  4782  raldifsni  4795  ssunpr  4834  sspr  4835  sstp  4836  uni0b  4933  uni0c  4934  ssint  4964  intprg  4981  iunssf  5044  iunss  5045  iundif2  5074  disjor  5125  nfnid  5375  reusv2lem4  5401  ssextss  5458  exss  5468  eqvinop  5492  sbcop  5494  opcom  5506  opeqpr  5510  brtp  5528  brabsb  5536  opelopabf  5550  dfid3  5581  pofun  5610  opeliunxp  5752  opeliun2xp  5753  xpiundi  5756  brinxp2  5763  reliun  5826  exopxfr  5854  cnvuni  5897  dmopab3  5930  rnep  5937  dmxp  5939  rnopab3  5967  elres  6038  elsnres  6039  elrid  6064  cnvsym  6132  cnvsymOLD  6133  asymref2  6137  intirr  6138  cnvopab  6157  xpeq0  6180  difxp  6184  xpdifid  6188  ssrnres  6198  dminxp  6200  dfrel4v  6210  elid  6219  dmsnn0  6227  imaco  6271  rnco  6272  coeq0  6275  resssxp  6290  dfpo2  6316  snres0  6318  sspred  6330  frpoind  6363  wfiOLD  6372  sb8iota  6525  dffun2OLDOLD  6573  fun11  6640  isarep1  6656  isarep1OLD  6657  dff1o4  6856  opabiota  6991  fvopab5  7049  eqfnfv3  7053  fvn0ssdmfun  7094  fnressn  7178  f13dfv  7294  dff1o6  7295  fliftel  7329  oprabidw  7462  oprabid  7463  eloprabga  7542  mpo2eqb  7565  ralrnmpo  7572  uniuni  7782  dflim3  7868  dfom2  7889  elxp4  7944  elxp5  7945  opabex3d  7990  opabex3rd  7991  opabex3  7992  el2xptp  8060  fsplit  8142  xporderlem  8152  ralxp3f  8162  frpoins3xpg  8165  poxp2  8168  suppvalbr  8189  dfrecs3  8412  dfrecs3OLD  8413  tz7.48lem  8481  seqomlem2  8491  oaord  8585  oeeu  8641  nnaord  8657  ecid  8822  mptelixpg  8975  elixpsn  8977  xpsnen  9095  xpcomco  9102  xpassen  9106  omxpenlem  9113  dom0OLD  9143  modom  9280  brttrcl2  9754  ttrcltr  9756  rnttrcl  9762  frind  9790  tz9.12lem3  9829  rankxpsuc  9922  cp  9931  cardprclem  10019  infxpenlem  10053  dfac5lem1  10163  dfac5lem2  10164  dfac5lem5  10167  dfac10c  10179  kmlem3  10193  kmlem12  10202  kmlem13  10203  kmlem14  10204  kmlem15  10205  ackbij2  10282  cf0  10291  cflim2  10303  dffin7-2  10438  dfacfin7  10439  fin1a2lem12  10451  axdc3lem3  10492  cfpwsdom  10624  recmulnq  11004  genpass  11049  psslinpr  11071  suplem2pr  11093  opelreal  11170  ltxrlt  11331  addrid  11441  elnn0  12528  elxnn0  12601  elnn0z  12626  nnwos  12957  elxr  13158  xrnepnf  13160  elfzuzb  13558  4fvwrd4  13688  preduz  13690  elfzo2  13702  ssnn0fi  14026  sqeqori  14253  xpcogend  15013  cotr2g  15015  fsumcom2  15810  modfsummod  15830  fprodcom2  16020  rpnnen2lem12  16261  gcdcllem1  16536  isprm2  16719  isprm7  16745  pythagtriplem2  16855  infpn2  16951  4sqlem12  16994  initoid  18046  termoid  18047  eldmcoa  18110  oduposb  18374  gsumwspan  18859  smndex1basss  18918  smndex1mgm  18920  isnsg2  19174  isnsg4  19185  cycsubmel  19218  efgcpbllemb  19773  dmdprd  20018  dprdval  20023  dprdw  20030  dprd2d2  20064  dfrhm2  20474  brric2  20506  issubrg  20571  isdomn5  20710  islmim  21061  lbsextlem2  21161  cnfldfun  21378  cnfldfunOLD  21391  pzriprnglem3  21494  pjfval2  21729  opsrtoslem1  22079  ntreq0  23085  cmpcov2  23398  cmpsub  23408  2ndcdisj  23464  unisngl  23535  txbas  23575  elpt  23580  txkgen  23660  xkococn  23668  fbun  23848  trfil2  23895  fin1aufil  23940  alexsubALTlem3  24057  cnextcn  24075  qustgplem  24129  eltsms  24141  ustn0  24229  fmucndlem  24300  metrest  24537  restmetu  24583  isclmp  25130  srabn  25394  ellogdm  26681  1cubr  26885  leibpilem2  26984  dmarea  27000  vmasum  27260  dchrelbas2  27281  2lgslem4  27450  nosupbnd1lem4  27756  nosupbnd2lem1  27760  slenlt  27797  madeval2  27892  made0  27912  tgcgr4  28539  ltgov  28605  axlowdimlem13  28969  axeuclidlem  28977  numedglnl  29161  nbupgrres  29381  vtxd0nedgb  29506  rusgrprc  29608  usgr2pth0  29785  wspthsnwspthsnon  29936  isclwwlk  30003  clwwlkn1  30060  clwwlkn2  30063  clwwlknonel  30114  3pthdlem1  30183  iseupthf1o  30221  frgr3v  30294  fusgr2wsp2nb  30353  frgrregord013  30414  h2hcau  30998  h2hlm  30999  shlesb1i  31405  shne0i  31467  chnlei  31504  cmbr2i  31615  pjneli  31742  ho02i  31848  adjsym  31852  adjeu  31908  lnopeqi  32027  largei  32286  atoml2i  32402  cdj3lem3b  32459  or3di  32478  mo5f  32508  dmrab  32516  rabsspr  32520  rabsstp  32521  disjnf  32583  disjorf  32592  ssrelf  32627  ofpreima  32675  disjdsct  32712  1stpreima  32716  2ndpreima  32717  f1od2  32732  xrdifh  32782  nndiffz1  32788  ind1a  32844  prmidl0  33478  zarclsun  33869  ordtconnlem1  33923  measiuns  34218  elunirnmbfm  34253  eulerpartlemr  34376  eulerpartlemgh  34380  eulerpartlemn  34383  ballotlemodife  34500  bnj250  34715  bnj334  34727  bnj345  34728  bnj89  34735  bnj115  34739  bnj919  34781  bnj1304  34833  bnj92  34876  bnj124  34885  bnj126  34887  bnj154  34892  bnj155  34893  bnj523  34901  bnj526  34902  bnj540  34906  bnj581  34922  bnj916  34947  bnj929  34950  bnj964  34957  bnj978  34963  bnj983  34965  bnj1039  34985  bnj1040  34986  bnj1123  35000  bnj1128  35004  bnj1398  35048  lfuhgr3  35125  cvmlift2lem1  35307  satfv0  35363  satf0  35377  satf0op  35382  satffunlem  35406  satffunlem1lem1  35407  satffunlem2lem1  35409  elmthm  35581  quad3  35675  3orit  35716  dftr6  35751  eldm3  35761  elrn3  35762  elima4  35776  19.12b  35802  brtxp  35881  brtxp2  35882  brpprod  35886  brpprod3a  35887  elfix  35904  dffix2  35906  ellimits  35911  sscoid  35914  dffun10  35915  elfuns  35916  elsingles  35919  brimg  35938  brapply  35939  brsuccf  35942  funpartlem  35943  brrestrict  35950  dfrecs2  35951  dfrdg4  35952  brlb  35956  altopthc  35972  altopthd  35973  fvtransport  36033  hfext  36184  ss-ax8  36226  nn0prpw  36324  filnetlem4  36382  df3nandALT2  36401  bj-sbeq  36902  bj-csbsnlem  36904  bj-elsngl  36969  bj-eltag  36978  bj-tagex  36988  bj-projun  36995  bj-reabeq  37028  bj-disj2r  37029  bj-restuni  37098  bj-elid6  37171  bj-eldiag  37177  bj-eldiag2  37178  topdifinffinlem  37348  relowlpssretop  37365  fvineqsneq  37413  wl-3xorbi  37474  wl-2mintru1  37491  wl-df3maxtru1  37493  wl-dfclab  37597  phpreu  37611  poimirlem24  37651  poimirlem26  37653  poimirlem30  37657  areacirclem5  37719  isbnd2  37790  sbcalf  38121  sbcexf  38122  sbccom2  38132  sbccom2f  38133  sbccom2fi  38134  csbcom2fi  38135  anan  38230  br1cnvinxp  38257  idinxpssinxp2  38319  ineleq  38355  brabidgaw  38366  brabidga  38367  inxpxrn  38396  rnxrn  38399  cossssid2  38469  cossssid3  38470  cosscnvssid3  38477  dfeldisj3  38720  dfeldisj4  38721  antisymrelres  38764  dfmembpart2  38771  mpet3  38837  cpet2  38838  prtlem70  38858  prtlem16  38870  ishlat2  39354  pmapglb  39772  polval2N  39908  dicelval3  41182  mapdordlem1a  41636  redvmptabs  42390  fimgmcyclem  42543  fimgmcyc  42544  prjspeclsp  42622  sn-isghm  42683  abbibw  42687  fz1eqin  42780  7rexfrabdioph  42811  rmydioph  43026  dford4  43041  areaquad  43228  onsupmaxb  43251  onov0suclim  43287  nnoeomeqom  43325  tfsconcat0i  43358  faosnf0.11b  43440  ifpan23  43473  ifpdfnan  43499  ifpdfxor  43500  ifpidg  43504  ifpid1g  43507  ifpim123g  43513  ifp1bi  43515  ifpimimb  43517  ifpororb  43518  ifpbibib  43523  rp-fakeuninass  43529  dfsucon  43536  minregex  43547  cllem0  43579  rababg  43587  elmapintrab  43589  elmapintab  43609  undmrnresiss  43617  dfxor4  43779  dfhe3  43788  dffrege115  43991  frege131  44007  frege133  44009  clsk1indlem4  44057  clsk1indlem1  44058  expandrexn  44310  rr-groth  44318  rr-grothshortbi  44322  undisjrab  44325  pm13.196a  44433  eelT11  44727  eelTT1  44730  eelT01  44731  eel0T1  44732  uunTT1  44813  uunTT1p1  44814  uunTT1p2  44815  uunT11  44816  uunT11p1  44817  uunT11p2  44818  uun111  44825  xpwf  44981  ssrabf  45119  rabssf  45124  disjinfi  45197  elicores  45546  fourierdlem42  46164  iundjiun  46475  2reu7  47123  2reu8  47124  2reu8i  47125  dfdfat2  47140  aovov0bi  47208  afv2orxorb  47240  afv2ndeffv0  47272  ichcircshi  47441  ichan  47442  icheq  47449  ichal  47453  prpair  47488  prproropf1olem0  47489  257prm  47548  fmtno4prmfac  47559  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  clnbgrel  47815  isubgr3stgrlem4  47936  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  uspgrsprf1  48063  rrx2xpref1o  48639  resinsn  48772  resinsnALT  48773  0funcALT  48921  isthincd2  49086  aacllem  49320