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  1501  excxor  1517  cadan  1610  cadcomb  1614  nic-axALT  1675  tbw-bijust  1699  rb-bijust  1750  nf2  1786  19.43  1883  19.43OLD  1884  3exdistr  1961  19.12vvv  1995  sbco4  2105  excom13  2167  sbcom2  2176  sbco4OLD  2178  sbn  2282  sbnf  2313  19.12vv  2347  eeeanv  2350  ee4anv  2351  ee4anvOLD  2352  2sb8ef  2356  sbel2x  2474  2sb8e  2530  dfmo  2591  sb8eulem  2593  2mo2  2642  2eu7  2653  2eu8  2654  sbabel  2927  3r19.43  3101  r19.23v  3159  2ralor  3206  rexcom13  3265  cbvreu  3387  rabrabi  3414  cgsex4g  3483  ceqsex2  3490  ceqsex2v  3491  ceqsex3v  3492  ceqsex4v  3493  ceqsex6v  3494  ceqsex8v  3495  ralrab2  3657  rexrab2  3659  reu2  3684  rmo4  3689  reu8  3692  rmo3f  3693  2reu5lem3  3716  sbcimdv  3810  reu8nf  3828  rmo2  3838  rmo3  3840  rmoanim  3845  ss2rab  4021  rabss  4022  ssrab  4023  dfdif3OLD  4068  symdifass  4212  dfss4  4219  undi  4235  indifdi  4244  undif3  4250  reuun2  4275  difin0ss  4323  disj  4400  disj4  4409  rabsssn  4621  disjsn  4664  snssb  4735  raldifsni  4747  ssunpr  4786  sspr  4787  sstp  4788  uni0b  4885  uni0c  4886  ssint  4914  intprg  4931  iunssf  4993  iunss  4994  iundif2  5022  disjor  5073  nfnid  5313  reusv2lem4  5339  ssextss  5394  exss  5403  eqvinop  5427  sbcop  5429  opcom  5441  opeqpr  5445  brtp  5463  brabsb  5471  opelopabf  5485  dfid3  5514  pofun  5542  opeliunxp  5683  opeliun2xp  5684  xpiundi  5687  brinxp2  5694  reliun  5756  exopxfr  5783  cnvuni  5826  dmopab3  5859  rnep  5867  dmxp  5869  rnopab3  5896  elres  5969  elsnres  5970  elrid  5995  cnvsym  6061  asymref2  6064  intirr  6065  cnvopab  6084  xpeq0  6107  difxp  6111  xpdifid  6115  ssrnres  6125  dminxp  6127  dfrel4v  6137  elid  6146  dmsnn0  6154  imaco  6198  rnco  6199  rncoOLD  6200  coeq0  6203  resssxp  6217  dfpo2  6243  snres0  6245  sspred  6257  frpoind  6289  sb8iota  6448  fun11  6555  isarep1  6570  dff1o4  6771  opabiota  6904  fvopab5  6962  eqfnfv3  6966  fvn0ssdmfun  7007  fnressn  7091  f13dfv  7208  dff1o6  7209  fliftel  7243  oprabidw  7377  oprabid  7378  eloprabga  7455  mpo2eqb  7478  ralrnmpo  7485  uniuni  7695  dflim3  7777  dfom2  7798  elxp4  7852  elxp5  7853  opabex3d  7897  opabex3rd  7898  opabex3  7899  el2xptp  7967  fsplit  8047  xporderlem  8057  ralxp3f  8067  frpoins3xpg  8070  poxp2  8073  suppvalbr  8094  dfrecs3  8292  tz7.48lem  8360  seqomlem2  8370  oaord  8462  oeeu  8518  nnaord  8534  ecid  8704  mptelixpg  8859  elixpsn  8861  xpsnen  8974  xpcomco  8980  xpassen  8984  omxpenlem  8991  modom  9135  brttrcl2  9604  ttrcltr  9606  rnttrcl  9612  frind  9643  tz9.12lem3  9682  rankxpsuc  9775  cp  9784  cardprclem  9872  infxpenlem  9904  dfac5lem1  10014  dfac5lem2  10015  dfac5lem5  10018  dfac10c  10030  kmlem3  10044  kmlem12  10053  kmlem13  10054  kmlem14  10055  kmlem15  10056  ackbij2  10133  cf0  10142  cflim2  10154  dffin7-2  10289  dfacfin7  10290  fin1a2lem12  10302  axdc3lem3  10343  cfpwsdom  10475  recmulnq  10855  genpass  10900  psslinpr  10922  suplem2pr  10944  opelreal  11021  ltxrlt  11183  addrid  11293  elnn0  12383  elxnn0  12456  elnn0z  12481  nnwos  12813  elxr  13015  xrnepnf  13017  elfzuzb  13418  4fvwrd4  13548  preduz  13550  elfzo2  13562  ssnn0fi  13892  sqeqori  14121  xpcogend  14881  cotr2g  14883  fsumcom2  15681  modfsummod  15701  fprodcom2  15891  rpnnen2lem12  16134  gcdcllem1  16410  isprm2  16593  isprm7  16619  pythagtriplem2  16729  infpn2  16825  4sqlem12  16868  initoid  17908  termoid  17909  eldmcoa  17972  oduposb  18233  gsumwspan  18754  smndex1basss  18813  smndex1mgm  18815  isnsg2  19069  isnsg4  19080  cycsubmel  19113  efgcpbllemb  19668  dmdprd  19913  dprdval  19918  dprdw  19925  dprd2d2  19959  dfrhm2  20393  brric2  20422  issubrg  20487  isdomn5  20626  islmim  20997  lbsextlem2  21097  cnfldfun  21306  cnfldfunOLD  21319  pzriprnglem3  21421  pjfval2  21647  opsrtoslem1  21991  ntreq0  22993  cmpcov2  23306  cmpsub  23316  2ndcdisj  23372  unisngl  23443  txbas  23483  elpt  23488  txkgen  23568  xkococn  23576  fbun  23756  trfil2  23803  fin1aufil  23848  alexsubALTlem3  23965  cnextcn  23983  qustgplem  24037  eltsms  24049  ustn0  24137  fmucndlem  24206  metrest  24440  restmetu  24486  isclmp  25025  srabn  25288  ellogdm  26576  1cubr  26780  leibpilem2  26879  dmarea  26895  vmasum  27155  dchrelbas2  27176  2lgslem4  27345  nosupbnd1lem4  27651  nosupbnd2lem1  27655  slenlt  27692  madeval2  27795  made0  27819  onsiso  28206  onsfi  28284  tgcgr4  28510  ltgov  28576  axlowdimlem13  28933  axeuclidlem  28941  numedglnl  29123  nbupgrres  29343  vtxd0nedgb  29468  rusgrprc  29570  usgr2pth0  29744  wspthsnwspthsnon  29895  isclwwlk  29962  clwwlkn1  30019  clwwlkn2  30022  clwwlknonel  30073  3pthdlem1  30142  iseupthf1o  30180  frgr3v  30253  fusgr2wsp2nb  30312  frgrregord013  30373  h2hcau  30957  h2hlm  30958  shlesb1i  31364  shne0i  31426  chnlei  31463  cmbr2i  31574  pjneli  31701  ho02i  31807  adjsym  31811  adjeu  31867  lnopeqi  31986  largei  32245  atoml2i  32361  cdj3lem3b  32418  or3di  32436  mo5f  32466  dmrab  32474  rabsspr  32479  rabsstp  32480  disjnf  32548  disjorf  32557  ssrelf  32596  ofpreima  32645  disjdsct  32682  1stpreima  32686  2ndpreima  32687  f1od2  32700  xrdifh  32761  nndiffz1  32767  ind1a  32838  prmidl0  33413  zarclsun  33881  ordtconnlem1  33935  measiuns  34228  elunirnmbfm  34263  eulerpartlemr  34385  eulerpartlemgh  34389  eulerpartlemn  34392  ballotlemodife  34509  bnj250  34711  bnj334  34723  bnj345  34724  bnj89  34731  bnj115  34735  bnj919  34777  bnj1304  34829  bnj92  34872  bnj124  34881  bnj126  34883  bnj154  34888  bnj155  34889  bnj523  34897  bnj526  34898  bnj540  34902  bnj581  34918  bnj916  34943  bnj929  34946  bnj964  34953  bnj978  34959  bnj983  34961  bnj1039  34981  bnj1040  34982  bnj1123  34996  bnj1128  35000  bnj1398  35044  lfuhgr3  35162  cvmlift2lem1  35344  satfv0  35400  satf0  35414  satf0op  35419  satffunlem  35443  satffunlem1lem1  35444  satffunlem2lem1  35446  elmthm  35618  quad3  35712  3orit  35758  dftr6  35793  eldm3  35803  elrn3  35804  elima4  35818  19.12b  35841  brtxp  35920  brtxp2  35921  brpprod  35925  brpprod3a  35926  elfix  35943  dffix2  35945  ellimits  35950  sscoid  35953  dffun10  35954  elfuns  35955  elsingles  35958  brimg  35977  brapply  35978  brsuccf  35981  funpartlem  35982  brrestrict  35989  dfrecs2  35990  dfrdg4  35991  brlb  35995  altopthc  36011  altopthd  36012  fvtransport  36072  hfext  36223  ss-ax8  36265  nn0prpw  36363  filnetlem4  36421  df3nandALT2  36440  bj-sbeq  36941  bj-csbsnlem  36943  bj-elsngl  37008  bj-eltag  37017  bj-tagex  37027  bj-projun  37034  bj-reabeq  37067  bj-disj2r  37068  bj-restuni  37137  bj-elid6  37210  bj-eldiag  37216  bj-eldiag2  37217  topdifinffinlem  37387  relowlpssretop  37404  fvineqsneq  37452  wl-3xorbi  37513  wl-2mintru1  37530  wl-df3maxtru1  37532  wl-dfclab  37636  phpreu  37650  poimirlem24  37690  poimirlem26  37692  poimirlem30  37696  areacirclem5  37758  isbnd2  37829  sbcalf  38160  sbcexf  38161  sbccom2  38171  sbccom2f  38172  sbccom2fi  38173  csbcom2fi  38174  anan  38269  br1cnvinxp  38297  idinxpssinxp2  38358  ineleq  38388  brabidgaw  38399  brabidga  38400  inxpxrn  38433  rnxrn  38436  cossssid2  38511  cossssid3  38512  cosscnvssid3  38519  dfeldisj3  38763  dfeldisj4  38764  antisymrelres  38807  dfmembpart2  38814  mpet3  38880  cpet2  38881  prtlem70  38902  prtlem16  38914  ishlat2  39398  pmapglb  39815  polval2N  39951  dicelval3  41225  mapdordlem1a  41679  redvmptabs  42399  fimgmcyclem  42572  fimgmcyc  42573  prjspeclsp  42651  sn-isghm  42712  abbibw  42716  fz1eqin  42808  7rexfrabdioph  42839  rmydioph  43053  dford4  43068  areaquad  43255  onsupmaxb  43278  onov0suclim  43313  nnoeomeqom  43351  tfsconcat0i  43384  faosnf0.11b  43466  ifpan23  43499  ifpdfnan  43525  ifpdfxor  43526  ifpidg  43530  ifpid1g  43533  ifpim123g  43539  ifp1bi  43541  ifpimimb  43543  ifpororb  43544  ifpbibib  43549  rp-fakeuninass  43555  dfsucon  43562  minregex  43573  cllem0  43605  rababg  43613  elmapintrab  43615  elmapintab  43635  undmrnresiss  43643  dfxor4  43805  dfhe3  43814  dffrege115  44017  frege131  44033  frege133  44035  clsk1indlem4  44083  clsk1indlem1  44084  expandrexn  44330  rr-groth  44338  rr-grothshortbi  44342  undisjrab  44345  pm13.196a  44453  eelT11  44745  eelTT1  44748  eelT01  44749  eel0T1  44750  uunTT1  44831  uunTT1p1  44832  uunTT1p2  44833  uunT11  44834  uunT11p1  44835  uunT11p2  44836  uun111  44843  xpwf  45003  permaxinf2lem  45051  permac8prim  45053  ssrabf  45157  rabssf  45162  disjinfi  45235  elicores  45579  fourierdlem42  46193  iundjiun  46504  2reu7  47148  2reu8  47149  2reu8i  47150  dfdfat2  47165  aovov0bi  47233  afv2orxorb  47265  afv2ndeffv0  47297  ichcircshi  47491  ichan  47492  icheq  47499  ichal  47503  prpair  47538  prproropf1olem0  47539  257prm  47598  fmtno4prmfac  47609  nnsum4primeseven  47837  nnsum4primesevenALTV  47838  clnbgrel  47865  isubgr3stgrlem4  48006  usgrexmpl2nb1  48069  usgrexmpl2nb2  48070  gpgprismgr4cycllem10  48141  uspgrsprf1  48184  rrx2xpref1o  48756  iinxp  48868  resinsn  48909  resinsnALT  48910  0funcALT  49126  catcsect  49436  isthincd2  49475  aacllem  49839