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  1486  nanbi  1502  excxor  1518  cadan  1611  cadcomb  1615  nic-axALT  1676  tbw-bijust  1700  rb-bijust  1751  nf2  1787  19.43  1884  19.43OLD  1885  3exdistr  1962  19.12vvv  1996  sbco4  2108  excom13  2170  sbcom2  2179  sbco4OLD  2181  sbn  2287  sbnf  2318  19.12vv  2351  eeeanv  2354  ee4anv  2355  ee4anvOLD  2356  2sb8ef  2360  sbel2x  2478  2sb8e  2534  dfmo2  2596  sb8eulem  2598  2mo2  2647  2eu7  2658  2eu8  2659  sbabel  2931  3r19.43  3106  r19.23v  3164  2ralor  3211  rexcom13  3270  cbvreu  3381  rabrabi  3408  cgsex4g  3476  ceqsex2  3481  ceqsex2v  3482  ceqsex3v  3483  ceqsex4v  3484  ceqsex6v  3485  ceqsex8v  3486  ralrab2  3644  rexrab2  3646  reu2  3671  rmo4  3676  reu8  3679  rmo3f  3680  2reu5lem3  3703  sbcimdv  3797  reu8nf  3815  rmo2  3825  rmo3  3827  rmoanim  3832  ss2rab  4009  rabss  4010  ssrab  4011  dfdif3OLD  4058  symdifass  4202  dfss4  4209  undi  4225  indifdi  4234  undif3  4240  reuun2  4265  difin0ss  4313  disj  4390  disj4  4399  rabsssn  4612  disjsn  4655  snssb  4726  raldifsni  4740  ssunpr  4777  sspr  4778  sstp  4779  uni0b  4876  uni0c  4877  ssint  4906  intprg  4923  iunssf  4985  iunssfOLD  4986  iunss  4987  iunssOLD  4988  iundif2  5016  disjor  5067  nfnid  5317  reusv2lem4  5343  ssextss  5405  exss  5415  eqvinop  5440  sbcop  5442  opcom  5455  opeqpr  5459  brtp  5478  brabsb  5486  opelopabf  5500  dfid3  5529  pofun  5557  opeliunxp  5698  opeliun2xp  5699  xpiundi  5702  brinxp2  5709  exopxfr  5798  cnvuni  5841  dmopab3  5874  rnep  5882  dmxp  5884  rnopab3  5911  elres  5985  elsnres  5986  elrid  6011  cnvsym  6077  asymref2  6080  intirr  6081  cnvopab  6100  xpeq0  6124  difxp  6128  xpdifid  6132  ssrnres  6142  dminxp  6144  dfrel4v  6154  elid  6163  dmsnn0  6171  imaco  6215  rnco  6216  rncoOLD  6217  coeq0  6220  resssxp  6234  dfpo2  6260  snres0  6262  sspred  6274  frpoind  6306  sb8iota  6465  fun11  6572  isarep1  6587  dff1o4  6788  opabiota  6922  fvopab5  6981  eqfnfv3  6985  fvn0ssdmfun  7026  fnressn  7112  f13dfv  7229  dff1o6  7230  fliftel  7264  oprabidw  7398  oprabid  7399  eloprabga  7476  mpo2eqb  7499  ralrnmpo  7506  uniuni  7716  dflim3  7798  dfom2  7819  elxp4  7873  elxp5  7874  opabex3d  7918  opabex3rd  7919  opabex3  7920  el2xptp  7988  fsplit  8067  xporderlem  8077  ralxp3f  8087  frpoins3xpg  8090  poxp2  8093  suppvalbr  8114  dfrecs3  8312  tz7.48lem  8380  seqomlem2  8390  oaord  8482  oeeu  8539  nnaord  8555  ecid  8727  mptelixpg  8883  elixpsn  8885  xpsnen  8999  xpcomco  9005  xpassen  9009  omxpenlem  9016  modom  9161  brttrcl2  9635  ttrcltr  9637  rnttrcl  9643  frind  9674  tz9.12lem3  9713  rankxpsuc  9806  cp  9815  cardprclem  9903  infxpenlem  9935  dfac5lem1  10045  dfac5lem2  10046  dfac5lem5  10049  dfac10c  10061  kmlem3  10075  kmlem12  10084  kmlem13  10085  kmlem14  10086  kmlem15  10087  ackbij2  10164  cf0  10173  cflim2  10185  dffin7-2  10320  dfacfin7  10321  fin1a2lem12  10333  axdc3lem3  10374  cfpwsdom  10507  recmulnq  10887  genpass  10932  psslinpr  10954  suplem2pr  10976  opelreal  11053  ltxrlt  11216  addrid  11326  ind1a  12170  elnn0  12439  elxnn0  12512  elnn0z  12537  nnwos  12865  elxr  13067  xrnepnf  13069  elfzuzb  13472  4fvwrd4  13602  preduz  13604  elfzo2  13616  ssnn0fi  13947  sqeqori  14176  xpcogend  14936  cotr2g  14938  fsumcom2  15736  modfsummod  15757  fprodcom2  15949  rpnnen2lem12  16192  gcdcllem1  16468  isprm2  16651  isprm7  16678  pythagtriplem2  16788  infpn2  16884  4sqlem12  16927  initoid  17968  termoid  17969  eldmcoa  18032  oduposb  18293  gsumwspan  18814  smndex1basss  18876  smndex1mgm  18878  isnsg2  19131  isnsg4  19142  cycsubmel  19175  efgcpbllemb  19730  dmdprd  19975  dprdval  19980  dprdw  19987  dprd2d2  20021  dfrhm2  20454  brric2  20483  issubrg  20548  isdomn5  20687  islmim  21057  lbsextlem2  21157  cnfldfun  21366  pzriprnglem3  21463  pjfval2  21689  opsrtoslem1  22033  ntreq0  23042  cmpcov2  23355  cmpsub  23365  2ndcdisj  23421  unisngl  23492  txbas  23532  elpt  23537  txkgen  23617  xkococn  23625  fbun  23805  trfil2  23852  fin1aufil  23897  alexsubALTlem3  24014  cnextcn  24032  qustgplem  24086  eltsms  24098  ustn0  24186  fmucndlem  24255  metrest  24489  restmetu  24535  isclmp  25064  srabn  25327  ellogdm  26603  1cubr  26806  leibpilem2  26905  dmarea  26921  vmasum  27179  dchrelbas2  27200  2lgslem4  27369  nosupbnd1lem4  27675  nosupbnd2lem1  27679  lenlts  27716  madeval2  27825  made0  27855  oniso  28263  onsfi  28348  tgcgr4  28599  ltgov  28665  axlowdimlem13  29023  axeuclidlem  29031  numedglnl  29213  nbupgrres  29433  vtxd0nedgb  29557  rusgrprc  29659  usgr2pth0  29833  wspthsnwspthsnon  29984  isclwwlk  30054  clwwlkn1  30111  clwwlkn2  30114  clwwlknonel  30165  3pthdlem1  30234  iseupthf1o  30272  frgr3v  30345  fusgr2wsp2nb  30404  frgrregord013  30465  h2hcau  31050  h2hlm  31051  shlesb1i  31457  shne0i  31519  chnlei  31556  cmbr2i  31667  pjneli  31794  ho02i  31900  adjsym  31904  adjeu  31960  lnopeqi  32079  largei  32338  atoml2i  32454  cdj3lem3b  32511  or3di  32528  mo5f  32558  dmrab  32566  rabsspr  32571  rabsstp  32572  disjnf  32640  disjorf  32649  ssrelf  32688  ofpreima  32738  disjdsct  32776  1stpreima  32780  2ndpreima  32781  f1od2  32792  xrdifh  32853  nndiffz1  32859  domnprodeq0  33337  prmidl0  33510  zarclsun  34014  ordtconnlem1  34068  measiuns  34361  elunirnmbfm  34396  eulerpartlemr  34518  eulerpartlemgh  34522  eulerpartlemn  34525  ballotlemodife  34642  bnj250  34844  bnj334  34856  bnj345  34857  bnj89  34864  bnj115  34868  bnj919  34910  bnj1304  34961  bnj92  35004  bnj124  35013  bnj126  35015  bnj154  35020  bnj155  35021  bnj523  35029  bnj526  35030  bnj540  35034  bnj581  35050  bnj916  35075  bnj929  35078  bnj964  35085  bnj978  35091  bnj983  35093  bnj1039  35113  bnj1040  35114  bnj1123  35128  bnj1128  35132  bnj1398  35176  lfuhgr3  35302  cvmlift2lem1  35484  satfv0  35540  satf0  35554  satf0op  35559  satffunlem  35583  satffunlem1lem1  35584  satffunlem2lem1  35586  elmthm  35758  quad3  35852  3orit  35898  dftr6  35933  eldm3  35943  elrn3  35944  elima4  35958  19.12b  35981  brtxp  36060  brtxp2  36061  brpprod  36065  brpprod3a  36066  elfix  36083  dffix2  36085  ellimits  36090  sscoid  36093  dffun10  36094  elfuns  36095  elsingles  36098  brimg  36117  brapply  36118  lemsuccf  36121  brsuccf  36122  funpartlem  36124  brrestrict  36131  dfrecs2  36132  dfrdg4  36133  brlb  36137  altopthc  36153  altopthd  36154  fvtransport  36214  hfext  36365  ss-ax8  36407  nn0prpw  36505  filnetlem4  36563  df3nandALT2  36582  regsfromregtco  36720  mh-prprimbi  36725  mh-regprimbi  36727  mh-infprim2bi  36729  mh-infprim3bi  36730  bj-sbeq  37208  bj-csbsnlem  37210  bj-elsngl  37275  bj-eltag  37284  bj-tagex  37294  bj-projun  37301  bj-reabeq  37334  bj-disj2r  37335  bj-axseprep  37381  bj-restuni  37409  bj-elid6  37484  bj-eldiag  37490  bj-eldiag2  37491  topdifinffinlem  37663  relowlpssretop  37680  fvineqsneq  37728  wl-3xorbi  37789  wl-2mintru1  37806  wl-df3maxtru1  37808  wl-dfclab  37910  phpreu  37925  poimirlem24  37965  poimirlem26  37967  poimirlem30  37971  areacirclem5  38033  isbnd2  38104  sbcalf  38435  sbcexf  38436  sbccom2  38446  sbccom2f  38447  sbccom2fi  38448  csbcom2fi  38449  anan  38556  br1cnvinxp  38580  idinxpssinxp2  38645  ineleq  38675  brabidgaw  38694  brabidga  38695  inxpxrn  38739  rnxrn  38742  dfsucmap3  38784  cossssid2  38879  cossssid3  38880  cosscnvssid3  38887  dfeldisj3  39132  dfeldisj4  39133  antisymrelres  39187  dfmembpart2  39194  mpet3  39271  cpet2  39272  prtlem70  39303  prtlem16  39315  ishlat2  39799  pmapglb  40216  polval2N  40352  dicelval3  41626  mapdordlem1a  42080  redvmptabs  42792  fimgmcyclem  42978  fimgmcyc  42979  prjspeclsp  43045  sn-isghm  43106  abbibw  43110  fz1eqin  43201  7rexfrabdioph  43228  rmydioph  43442  dford4  43457  areaquad  43644  onsupmaxb  43667  onov0suclim  43702  nnoeomeqom  43740  tfsconcat0i  43773  faosnf0.11b  43854  ifpan23  43887  ifpdfnan  43913  ifpdfxor  43914  ifpidg  43918  ifpid1g  43921  ifpim123g  43927  ifp1bi  43929  ifpimimb  43931  ifpororb  43932  ifpbibib  43937  rp-fakeuninass  43943  dfsucon  43950  minregex  43961  cllem0  43993  rababg  44001  elmapintrab  44003  elmapintab  44023  undmrnresiss  44031  dfxor4  44193  dfhe3  44202  dffrege115  44405  frege131  44421  frege133  44423  clsk1indlem4  44471  clsk1indlem1  44472  expandrexn  44718  rr-groth  44726  rr-grothshortbi  44730  undisjrab  44733  pm13.196a  44841  eelT11  45133  eelTT1  45136  eelT01  45137  eel0T1  45138  uunTT1  45219  uunTT1p1  45220  uunTT1p2  45221  uunT11  45222  uunT11p1  45223  uunT11p2  45224  uun111  45231  xpwf  45391  permaxinf2lem  45439  permac8prim  45441  ssrabf  45544  rabssf  45549  disjinfi  45622  elicores  45963  fourierdlem42  46577  iundjiun  46888  2reu7  47559  2reu8  47560  2reu8i  47561  dfdfat2  47576  aovov0bi  47644  afv2orxorb  47676  afv2ndeffv0  47708  ichcircshi  47914  ichan  47915  icheq  47922  ichal  47926  prpair  47961  prproropf1olem0  47962  257prm  48024  fmtno4prmfac  48035  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  clnbgrel  48304  isubgr3stgrlem4  48445  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  gpgprismgr4cycllem10  48580  uspgrsprf1  48623  rrx2xpref1o  49194  iinxp  49306  resinsn  49347  resinsnALT  49348  0funcALT  49563  catcsect  49873  isthincd2  49912  aacllem  50276