Theorem 3bitri 300

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 278	. 2 ⊢ (𝜓 ↔ 𝜃)
5	1, 4	bitri 278	1 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  bibi1i  342  pm5.32  577  biadan  819  orbi1i  914  orass  922  or32  926  cases  1043  dn1  1058  3anidm  1106  an3andi  1484  an33rean  1485  an33reanOLD  1486  nanbi  1496  excxor  1513  norassOLD  1540  cadan  1616  cadcomb  1620  nic-axALT  1682  tbw-bijust  1706  rb-bijust  1757  nf2  1793  19.43  1890  19.43OLD  1891  3exdistr  1969  19.12vvv  1998  sbcom2  2167  excom13  2170  sbco4  2281  sbn  2283  19.12vv  2349  eeeanv  2352  ee4anv  2353  2sb8ev  2356  sbel2x  2473  2sb8e  2534  dfmo  2595  sb8eulem  2597  2mo2  2648  2eu7  2658  2eu8  2659  r19.26-3  3084  r19.23v  3188  rexcom  3258  ralcom13  3261  rexcom13  3262  cbvreuw  3341  cbvreu  3346  ceqsralt  3429  ceqsalv  3433  ceqsex2  3448  ceqsex2v  3449  ceqsex4v  3451  ralrab2  3601  rexrab2  3604  reu2  3627  rmo4  3632  reu8  3635  rmo3f  3636  2reu5lem3  3659  sbc3an  3752  sbcimdv  3756  reu8nf  3776  rmo2  3786  rmo3  3788  rmoanim  3793  dfss2OLD  3874  ss2rab  3970  rabss  3971  ssrab  3972  dfdif3  4015  symdifass  4152  dfss4  4159  undi  4175  indifdi  4184  undif3  4191  difin2  4192  difin0ss  4269  ab0OLD  4276  disj  4348  disjOLD  4349  disj4  4359  rabsssn  4569  disjsn  4613  raldifsni  4694  ssunpr  4731  sspr  4732  sstp  4733  uni0b  4833  uni0c  4834  ssint  4861  intprg  4878  iunssf  4939  iunss  4940  iundif2  4968  disjor  5019  nfnid  5253  reusv2lem4  5279  ssextss  5323  exss  5332  eqvinop  5355  sbcop  5357  opcom  5369  opeqpr  5373  brabsb  5397  opelopabf  5411  dfid3  5442  pofun  5471  opeliunxp  5601  xpiundi  5604  brinxp2  5611  reliun  5671  exopxfr  5697  cnvuni  5740  dmopab3  5773  rnep  5781  elres  5875  elsnres  5876  elrid  5898  asymref2  5962  intirr  5963  xpeq0  6003  xpdifid  6011  ssrnres  6021  dminxp  6023  dfrel4v  6033  elid  6042  dmsnn0  6050  rnco  6096  coeq0  6099  resssxp  6113  sspred  6148  frpoind  6174  wfi  6181  sb8iota  6328  dffun2  6368  fun11  6432  isarep1  6446  dff1o4  6647  opabiota  6772  fvopab5  6828  eqfnfv3  6832  fvn0ssdmfun  6873  fnressn  6951  f13dfv  7063  dff1o6  7064  fliftel  7096  oprabidw  7222  oprabid  7223  eloprabga  7296  mpo2eqb  7320  ralrnmpo  7326  uniuni  7525  dflim3  7604  dfom2  7624  elxp4  7678  elxp5  7679  opabex3d  7716  opabex3rd  7717  opabex3  7718  el2xptp  7785  fsplit  7863  xporderlem  7872  dfrecs3  8087  tz7.48lem  8155  seqomlem2  8165  oaord  8253  oeeu  8309  nnaord  8325  ecid  8442  mptelixpg  8594  elixpsn  8596  xpsnen  8707  xpcomco  8713  xpassen  8717  omxpenlem  8724  dom0  8752  modom  8855  tz9.12lem3  9370  rankxpsuc  9463  cp  9472  cardprclem  9560  infxpenlem  9592  dfac5lem1  9702  dfac5lem2  9703  dfac5lem5  9706  dfac10c  9717  kmlem3  9731  kmlem12  9740  kmlem13  9741  kmlem14  9742  kmlem15  9743  ackbij2  9822  cf0  9830  cflim2  9842  dffin7-2  9977  dfacfin7  9978  fin1a2lem12  9990  axdc3lem3  10031  cfpwsdom  10163  recmulnq  10543  genpass  10588  psslinpr  10610  suplem2pr  10632  opelreal  10709  ltxrlt  10868  addid1  10977  elnn0  12057  elxnn0  12129  elnn0z  12154  nnwos  12476  elxr  12673  xrnepnf  12675  elfzuzb  13071  4fvwrd4  13197  preduz  13199  elfzo2  13211  ssnn0fi  13523  sqeqori  13747  xpcogend  14502  cotr2g  14504  fsumcom2  15301  modfsummod  15321  fprodcom2  15509  rpnnen2lem12  15749  gcdcllem1  16021  isprm2  16202  isprm7  16228  pythagtriplem2  16333  infpn2  16429  4sqlem12  16472  initoid  17461  termoid  17462  eldmcoa  17525  oduposb  17789  gsumwspan  18227  smndex1basss  18286  smndex1mgm  18288  isnsg2  18526  isnsg4  18537  cycsubmel  18561  efgcpbllemb  19099  dmdprd  19339  dprdval  19344  dprdw  19351  dprd2d2  19385  dfrhm2  19691  brric2  19719  issubrg  19754  islmim  20053  lbsextlem2  20150  cnfldfunALT  20330  pjfval2  20625  opsrtoslem1  20966  ntreq0  21928  cmpcov2  22241  cmpsub  22251  2ndcdisj  22307  unisngl  22378  txbas  22418  elpt  22423  txkgen  22503  xkococn  22511  fbun  22691  trfil2  22738  fin1aufil  22783  alexsubALTlem3  22900  cnextcn  22918  qustgplem  22972  eltsms  22984  ustn0  23072  fmucndlem  23142  metrest  23376  restmetu  23422  isclmp  23948  srabn  24211  ellogdm  25481  1cubr  25679  leibpilem2  25778  dmarea  25794  vmasum  26051  dchrelbas2  26072  2lgslem4  26241  tgcgr4  26576  ltgov  26642  axlowdimlem13  26999  axeuclidlem  27007  numedglnl  27189  nbupgrres  27406  vtxd0nedgb  27530  rusgrprc  27632  usgr2pth0  27806  wspthsnwspthsnon  27954  isclwwlk  28021  clwwlkn1  28078  clwwlkn2  28081  clwwlknonel  28132  3pthdlem1  28201  iseupthf1o  28239  frgr3v  28312  fusgr2wsp2nb  28371  frgrregord013  28432  h2hcau  29014  h2hlm  29015  shlesb1i  29421  shne0i  29483  chnlei  29520  cmbr2i  29631  pjneli  29758  ho02i  29864  adjsym  29868  adjeu  29924  lnopeqi  30043  largei  30302  atoml2i  30418  cdj3lem3b  30475  or3di  30483  mo5f  30510  dmrab  30517  disjnf  30582  disjorf  30591  ssrelf  30628  ofpreima  30676  disjdsct  30709  1stpreima  30713  2ndpreima  30714  f1od2  30730  xrdifh  30775  nndiffz1  30781  prmidl0  31294  zarclsun  31488  ordtconnlem1  31542  ind1a  31653  measiuns  31851  elunirnmbfm  31886  eulerpartlemr  32007  eulerpartlemgh  32011  eulerpartlemn  32014  ballotlemodife  32130  bnj250  32346  bnj334  32358  bnj345  32359  bnj89  32366  bnj115  32370  bnj919  32413  bnj1304  32466  bnj92  32509  bnj124  32518  bnj126  32520  bnj154  32525  bnj155  32526  bnj523  32534  bnj526  32535  bnj540  32539  bnj581  32555  bnj916  32580  bnj929  32583  bnj964  32590  bnj978  32596  bnj983  32598  bnj1039  32618  bnj1040  32619  bnj1123  32633  bnj1128  32637  bnj1398  32681  lfuhgr3  32748  cvmlift2lem1  32931  satfv0  32987  satf0  33001  satf0op  33006  satffunlem  33030  satffunlem1lem1  33031  satffunlem2lem1  33033  elmthm  33205  quad3  33295  3orit  33327  snres0  33344  ralxp3f  33355  brtp  33386  dftr6  33387  dfpo2  33392  eldm3  33398  elrn3  33399  elima4  33420  19.12b  33447  frpoins3xpg  33457  frind  33460  poxp2  33470  nosupbnd1lem4  33600  nosupbnd2lem1  33604  slenlt  33641  madeval2  33723  made0  33743  brtxp  33868  brtxp2  33869  brpprod  33873  brpprod3a  33874  elfix  33891  dffix2  33893  ellimits  33898  sscoid  33901  dffun10  33902  elfuns  33903  elsingles  33906  brimg  33925  brapply  33926  brsuccf  33929  funpartlem  33930  brrestrict  33937  dfrecs2  33938  dfrdg4  33939  brlb  33943  altopthc  33959  altopthd  33960  fvtransport  34020  hfext  34171  nn0prpw  34198  filnetlem4  34256  df3nandALT2  34275  bj-sbeq  34773  bj-csbsnlem  34775  bj-elsngl  34844  bj-eltag  34853  bj-tagex  34863  bj-projun  34870  bj-reabeq  34903  bj-disj2r  34904  bj-restuni  34952  bj-elid6  35025  bj-eldiag  35031  bj-eldiag2  35032  topdifinffinlem  35204  relowlpssretop  35221  fvineqsneq  35269  wl-3xorbi  35330  wl-2mintru1  35347  wl-df3maxtru1  35349  wl-dfclab  35433  phpreu  35447  poimirlem24  35487  poimirlem26  35489  poimirlem30  35493  areacirclem5  35555  isbnd2  35627  sbcalf  35958  sbcexf  35959  sbccom2  35969  sbccom2f  35970  sbccom2fi  35971  csbcom2fi  35972  anan  36065  idinxpssinxp2  36139  ineleq  36172  brabidgaw  36181  brabidga  36182  inxpxrn  36207  rnxrn  36210  cossssid2  36272  cossssid3  36273  cosscnvssid3  36280  dfeldisj3  36516  dfeldisj4  36517  prtlem70  36557  prtlem16  36569  ishlat2  37053  pmapglb  37470  polval2N  37606  dicelval3  38880  mapdordlem1a  39334  isdomn5  39834  prjspeclsp  40100  fz1eqin  40235  7rexfrabdioph  40266  rmydioph  40480  dford4  40495  areaquad  40691  ifpan23  40693  ifpdfnan  40719  ifpdfxor  40720  ifpidg  40724  ifpid1g  40727  ifpim123g  40733  ifp1bi  40735  ifpimimb  40737  ifpororb  40738  ifpbibib  40743  rp-fakeuninass  40749  dfsucon  40756  cllem0  40790  rababg  40798  elmapintrab  40801  elmapintab  40821  undmrnresiss  40829  ss2iundf  40885  dfxor4  40992  dfhe3  41001  dffrege115  41204  frege131  41220  frege133  41222  clsk1indlem4  41272  clsk1indlem1  41273  expandrexn  41523  rr-groth  41531  rr-grothshortbi  41535  undisjrab  41538  pm13.196a  41646  eelT11  41941  eelTT1  41944  eelT01  41945  eel0T1  41946  uunTT1  42027  uunTT1p1  42028  uunTT1p2  42029  uunT11  42030  uunT11p1  42031  uunT11p2  42032  uun111  42039  ssrabf  42278  rabssf  42282  disjinfi  42345  elicores  42687  fourierdlem42  43308  iundjiun  43616  2reu7  44218  2reu8  44219  2reu8i  44220  dfdfat2  44235  aovov0bi  44303  afv2orxorb  44335  afv2ndeffv0  44367  ichcircshi  44522  ichan  44523  icheq  44530  ichal  44534  prpair  44569  prproropf1olem0  44570  257prm  44629  fmtno4prmfac  44640  nnsum4primeseven  44868  nnsum4primesevenALTV  44869  uspgrsprf1  44925  opeliun2xp  45284  rrx2xpref1o  45680  isthincd2  45935  aacllem  46119