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 205

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 206

This theorem is referenced by:  bibi1i  339  pm5.32  575  biadan  818  orbi1i  913  orass  921  or32  925  cases  1042  dn1  1057  3anidm  1105  an3andi  1483  an33rean  1484  an33reanOLD  1485  nanbi  1499  excxor  1516  cadan  1611  cadcomb  1615  nic-axALT  1677  tbw-bijust  1701  rb-bijust  1752  nf2  1788  19.43  1886  19.43OLD  1887  3exdistr  1965  19.12vvv  1993  sbcom2  2162  excom13  2165  sbco4  2275  sbn  2277  19.12vv  2344  eeeanv  2347  ee4anv  2348  2sb8ef  2353  sbel2x  2474  2sb8e  2530  dfmo  2591  sb8eulem  2593  2mo2  2644  2eu7  2654  2eu8  2655  sbabel  2939  r19.26-3  3113  r19.23v  3183  2ralor  3229  rexcomOLD  3289  ralcom13OLD  3293  rexcom13  3294  cbvreuwOLD  3413  cbvreu  3425  rabrabi  3451  cgsex4g  3521  ceqsex2  3530  ceqsex2v  3531  ceqsex3v  3532  ceqsex4v  3533  ceqsex6v  3534  ceqsex8v  3535  ralrab2  3695  rexrab2  3697  reu2  3722  rmo4  3727  reu8  3730  rmo3f  3731  2reu5lem3  3754  sbc3an  3848  sbcimdv  3852  reu8nf  3872  rmo2  3882  rmo3  3884  rmoanim  3889  dfss2OLD  3970  ss2rab  4069  rabss  4070  ssrab  4071  dfdif3  4115  symdifass  4252  dfss4  4259  undi  4275  indifdi  4284  undif3  4291  difin2  4292  difin0ss  4369  ab0OLD  4376  disj  4448  disjOLD  4449  disj4  4459  rabsssn  4671  disjsn  4716  snssb  4787  raldifsni  4799  ssunpr  4836  sspr  4837  sstp  4838  uni0b  4938  uni0c  4939  ssint  4969  intprg  4986  iunssf  5048  iunss  5049  iundif2  5078  disjor  5129  nfnid  5374  reusv2lem4  5400  ssextss  5454  exss  5464  eqvinop  5488  sbcop  5490  opcom  5502  opeqpr  5506  brtp  5524  brabsb  5532  opelopabf  5546  dfid3  5578  pofun  5607  opeliunxp  5744  xpiundi  5747  brinxp2  5754  reliun  5817  exopxfr  5844  cnvuni  5887  dmopab3  5920  rnep  5927  elres  6021  elsnres  6022  elrid  6046  cnvsym  6114  cnvsymOLD  6115  asymref2  6119  intirr  6120  xpeq0  6160  xpdifid  6168  ssrnres  6178  dminxp  6180  dfrel4v  6190  elid  6199  dmsnn0  6207  rnco  6252  coeq0  6255  resssxp  6270  dfpo2  6296  snres0  6298  sspred  6310  frpoind  6344  wfiOLD  6353  sb8iota  6508  dffun2OLDOLD  6556  fun11  6623  isarep1  6638  isarep1OLD  6639  dff1o4  6842  opabiota  6975  fvopab5  7031  eqfnfv3  7035  fvn0ssdmfun  7077  fnressn  7156  f13dfv  7272  dff1o6  7273  fliftel  7306  oprabidw  7440  oprabid  7441  eloprabga  7516  mpo2eqb  7541  ralrnmpo  7547  uniuni  7749  dflim3  7836  dfom2  7857  elxp4  7913  elxp5  7914  opabex3d  7952  opabex3rd  7953  opabex3  7954  el2xptp  8021  fsplit  8103  xporderlem  8113  ralxp3f  8123  frpoins3xpg  8126  poxp2  8129  suppvalbr  8150  dfrecs3  8372  dfrecs3OLD  8373  tz7.48lem  8441  seqomlem2  8451  oaord  8547  oeeu  8603  nnaord  8619  ecid  8776  mptelixpg  8929  elixpsn  8931  xpsnen  9055  xpcomco  9062  xpassen  9066  omxpenlem  9073  dom0OLD  9103  modom  9244  brttrcl2  9709  ttrcltr  9711  rnttrcl  9717  frind  9745  tz9.12lem3  9784  rankxpsuc  9877  cp  9886  cardprclem  9974  infxpenlem  10008  dfac5lem1  10118  dfac5lem2  10119  dfac5lem5  10122  dfac10c  10133  kmlem3  10147  kmlem12  10156  kmlem13  10157  kmlem14  10158  kmlem15  10159  ackbij2  10238  cf0  10246  cflim2  10258  dffin7-2  10393  dfacfin7  10394  fin1a2lem12  10406  axdc3lem3  10447  cfpwsdom  10579  recmulnq  10959  genpass  11004  psslinpr  11026  suplem2pr  11048  opelreal  11125  ltxrlt  11284  addrid  11394  elnn0  12474  elxnn0  12546  elnn0z  12571  nnwos  12899  elxr  13096  xrnepnf  13098  elfzuzb  13495  4fvwrd4  13621  preduz  13623  elfzo2  13635  ssnn0fi  13950  sqeqori  14178  xpcogend  14921  cotr2g  14923  fsumcom2  15720  modfsummod  15740  fprodcom2  15928  rpnnen2lem12  16168  gcdcllem1  16440  isprm2  16619  isprm7  16645  pythagtriplem2  16750  infpn2  16846  4sqlem12  16889  initoid  17951  termoid  17952  eldmcoa  18015  oduposb  18282  gsumwspan  18727  smndex1basss  18786  smndex1mgm  18788  isnsg2  19036  isnsg4  19047  cycsubmel  19077  efgcpbllemb  19623  dmdprd  19868  dprdval  19873  dprdw  19880  dprd2d2  19914  dfrhm2  20253  brric2  20285  issubrg  20319  islmim  20673  lbsextlem2  20772  isdomn5  20917  cnfldfun  20956  pjfval2  21264  opsrtoslem1  21616  ntreq0  22581  cmpcov2  22894  cmpsub  22904  2ndcdisj  22960  unisngl  23031  txbas  23071  elpt  23076  txkgen  23156  xkococn  23164  fbun  23344  trfil2  23391  fin1aufil  23436  alexsubALTlem3  23553  cnextcn  23571  qustgplem  23625  eltsms  23637  ustn0  23725  fmucndlem  23796  metrest  24033  restmetu  24079  isclmp  24613  srabn  24877  ellogdm  26147  1cubr  26347  leibpilem2  26446  dmarea  26462  vmasum  26719  dchrelbas2  26740  2lgslem4  26909  nosupbnd1lem4  27214  nosupbnd2lem1  27218  slenlt  27255  madeval2  27348  made0  27368  tgcgr4  27782  ltgov  27848  axlowdimlem13  28212  axeuclidlem  28220  numedglnl  28404  nbupgrres  28621  vtxd0nedgb  28745  rusgrprc  28847  usgr2pth0  29022  wspthsnwspthsnon  29170  isclwwlk  29237  clwwlkn1  29294  clwwlkn2  29297  clwwlknonel  29348  3pthdlem1  29417  iseupthf1o  29455  frgr3v  29528  fusgr2wsp2nb  29587  frgrregord013  29648  h2hcau  30232  h2hlm  30233  shlesb1i  30639  shne0i  30701  chnlei  30738  cmbr2i  30849  pjneli  30976  ho02i  31082  adjsym  31086  adjeu  31142  lnopeqi  31261  largei  31520  atoml2i  31636  cdj3lem3b  31693  or3di  31701  mo5f  31729  dmrab  31737  disjnf  31801  disjorf  31810  ssrelf  31844  ofpreima  31890  disjdsct  31924  1stpreima  31928  2ndpreima  31929  f1od2  31946  xrdifh  31991  nndiffz1  31997  prmidl0  32569  zarclsun  32850  ordtconnlem1  32904  ind1a  33017  measiuns  33215  elunirnmbfm  33250  eulerpartlemr  33373  eulerpartlemgh  33377  eulerpartlemn  33380  ballotlemodife  33496  bnj250  33712  bnj334  33724  bnj345  33725  bnj89  33732  bnj115  33736  bnj919  33778  bnj1304  33830  bnj92  33873  bnj124  33882  bnj126  33884  bnj154  33889  bnj155  33890  bnj523  33898  bnj526  33899  bnj540  33903  bnj581  33919  bnj916  33944  bnj929  33947  bnj964  33954  bnj978  33960  bnj983  33962  bnj1039  33982  bnj1040  33983  bnj1123  33997  bnj1128  34001  bnj1398  34045  lfuhgr3  34110  cvmlift2lem1  34293  satfv0  34349  satf0  34363  satf0op  34368  satffunlem  34392  satffunlem1lem1  34393  satffunlem2lem1  34395  elmthm  34567  quad3  34655  3orit  34685  dftr6  34721  eldm3  34731  elrn3  34732  elima4  34747  19.12b  34773  brtxp  34852  brtxp2  34853  brpprod  34857  brpprod3a  34858  elfix  34875  dffix2  34877  ellimits  34882  sscoid  34885  dffun10  34886  elfuns  34887  elsingles  34890  brimg  34909  brapply  34910  brsuccf  34913  funpartlem  34914  brrestrict  34921  dfrecs2  34922  dfrdg4  34923  brlb  34927  altopthc  34943  altopthd  34944  fvtransport  35004  hfext  35155  nn0prpw  35208  filnetlem4  35266  df3nandALT2  35285  bj-sbeq  35781  bj-csbsnlem  35783  bj-elsngl  35849  bj-eltag  35858  bj-tagex  35868  bj-projun  35875  bj-reabeq  35908  bj-disj2r  35909  bj-restuni  35978  bj-elid6  36051  bj-eldiag  36057  bj-eldiag2  36058  topdifinffinlem  36228  relowlpssretop  36245  fvineqsneq  36293  wl-3xorbi  36354  wl-2mintru1  36371  wl-df3maxtru1  36373  wl-dfclab  36458  phpreu  36472  poimirlem24  36512  poimirlem26  36514  poimirlem30  36518  areacirclem5  36580  isbnd2  36651  sbcalf  36982  sbcexf  36983  sbccom2  36993  sbccom2f  36994  sbccom2fi  36995  csbcom2fi  36996  anan  37093  br1cnvinxp  37124  idinxpssinxp2  37187  ineleq  37223  brabidgaw  37234  brabidga  37235  inxpxrn  37265  rnxrn  37268  cossssid2  37338  cossssid3  37339  cosscnvssid3  37346  dfeldisj3  37589  dfeldisj4  37590  antisymrelres  37633  dfmembpart2  37640  mpet3  37706  cpet2  37707  prtlem70  37727  prtlem16  37739  ishlat2  38223  pmapglb  38641  polval2N  38777  dicelval3  40051  mapdordlem1a  40505  prjspeclsp  41354  fz1eqin  41507  7rexfrabdioph  41538  rmydioph  41753  dford4  41768  areaquad  41965  onsupmaxb  41988  onov0suclim  42024  nnoeomeqom  42062  tfsconcat0i  42095  faosnf0.11b  42178  ifpan23  42211  ifpdfnan  42237  ifpdfxor  42238  ifpidg  42242  ifpid1g  42245  ifpim123g  42251  ifp1bi  42253  ifpimimb  42255  ifpororb  42256  ifpbibib  42261  rp-fakeuninass  42267  dfsucon  42274  minregex  42285  cllem0  42317  rababg  42325  elmapintrab  42327  elmapintab  42347  undmrnresiss  42355  dfxor4  42517  dfhe3  42526  dffrege115  42729  frege131  42745  frege133  42747  clsk1indlem4  42795  clsk1indlem1  42796  expandrexn  43050  rr-groth  43058  rr-grothshortbi  43062  undisjrab  43065  pm13.196a  43173  eelT11  43468  eelTT1  43471  eelT01  43472  eel0T1  43473  uunTT1  43554  uunTT1p1  43555  uunTT1p2  43556  uunT11  43557  uunT11p1  43558  uunT11p2  43559  uun111  43566  ssrabf  43803  rabssf  43808  disjinfi  43891  elicores  44246  fourierdlem42  44865  iundjiun  45176  2reu7  45819  2reu8  45820  2reu8i  45821  dfdfat2  45836  aovov0bi  45904  afv2orxorb  45936  afv2ndeffv0  45968  ichcircshi  46122  ichan  46123  icheq  46130  ichal  46134  prpair  46169  prproropf1olem0  46170  257prm  46229  fmtno4prmfac  46240  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  uspgrsprf1  46525  pzriprnglem3  46807  opeliun2xp  47008  rrx2xpref1o  47404  isthincd2  47658  aacllem  47848