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  3694  rexrab2  3696  reu2  3721  rmo4  3726  reu8  3729  rmo3f  3730  2reu5lem3  3753  sbc3an  3847  sbcimdv  3851  reu8nf  3871  rmo2  3881  rmo3  3883  rmoanim  3888  dfss2OLD  3969  ss2rab  4068  rabss  4069  ssrab  4070  dfdif3  4114  symdifass  4251  dfss4  4258  undi  4274  indifdi  4283  undif3  4290  difin2  4291  difin0ss  4368  ab0OLD  4375  disj  4447  disjOLD  4448  disj4  4458  rabsssn  4670  disjsn  4715  snssb  4786  raldifsni  4798  ssunpr  4835  sspr  4836  sstp  4837  uni0b  4937  uni0c  4938  ssint  4968  intprg  4985  iunssf  5047  iunss  5048  iundif2  5077  disjor  5128  nfnid  5373  reusv2lem4  5399  ssextss  5453  exss  5463  eqvinop  5487  sbcop  5489  opcom  5501  opeqpr  5505  brtp  5523  brabsb  5531  opelopabf  5545  dfid3  5577  pofun  5606  opeliunxp  5742  xpiundi  5745  brinxp2  5752  reliun  5815  exopxfr  5842  cnvuni  5885  dmopab3  5918  rnep  5925  elres  6019  elsnres  6020  elrid  6044  cnvsym  6111  cnvsymOLD  6112  asymref2  6116  intirr  6117  xpeq0  6157  xpdifid  6165  ssrnres  6175  dminxp  6177  dfrel4v  6187  elid  6196  dmsnn0  6204  rnco  6249  coeq0  6252  resssxp  6267  dfpo2  6293  snres0  6295  sspred  6307  frpoind  6341  wfiOLD  6350  sb8iota  6505  dffun2OLDOLD  6553  fun11  6620  isarep1  6635  isarep1OLD  6636  dff1o4  6839  opabiota  6972  fvopab5  7028  eqfnfv3  7032  fvn0ssdmfun  7074  fnressn  7153  f13dfv  7269  dff1o6  7270  fliftel  7303  oprabidw  7437  oprabid  7438  eloprabga  7513  mpo2eqb  7538  ralrnmpo  7544  uniuni  7746  dflim3  7833  dfom2  7854  elxp4  7910  elxp5  7911  opabex3d  7949  opabex3rd  7950  opabex3  7951  el2xptp  8018  fsplit  8100  xporderlem  8110  ralxp3f  8120  frpoins3xpg  8123  poxp2  8126  suppvalbr  8147  dfrecs3  8369  dfrecs3OLD  8370  tz7.48lem  8438  seqomlem2  8448  oaord  8544  oeeu  8600  nnaord  8616  ecid  8773  mptelixpg  8926  elixpsn  8928  xpsnen  9052  xpcomco  9059  xpassen  9063  omxpenlem  9070  dom0OLD  9100  modom  9241  brttrcl2  9706  ttrcltr  9708  rnttrcl  9714  frind  9742  tz9.12lem3  9781  rankxpsuc  9874  cp  9883  cardprclem  9971  infxpenlem  10005  dfac5lem1  10115  dfac5lem2  10116  dfac5lem5  10119  dfac10c  10130  kmlem3  10144  kmlem12  10153  kmlem13  10154  kmlem14  10155  kmlem15  10156  ackbij2  10235  cf0  10243  cflim2  10255  dffin7-2  10390  dfacfin7  10391  fin1a2lem12  10403  axdc3lem3  10444  cfpwsdom  10576  recmulnq  10956  genpass  11001  psslinpr  11023  suplem2pr  11045  opelreal  11122  ltxrlt  11281  addrid  11391  elnn0  12471  elxnn0  12543  elnn0z  12568  nnwos  12896  elxr  13093  xrnepnf  13095  elfzuzb  13492  4fvwrd4  13618  preduz  13620  elfzo2  13632  ssnn0fi  13947  sqeqori  14175  xpcogend  14918  cotr2g  14920  fsumcom2  15717  modfsummod  15737  fprodcom2  15925  rpnnen2lem12  16165  gcdcllem1  16437  isprm2  16616  isprm7  16642  pythagtriplem2  16747  infpn2  16843  4sqlem12  16886  initoid  17948  termoid  17949  eldmcoa  18012  oduposb  18279  gsumwspan  18724  smndex1basss  18783  smndex1mgm  18785  isnsg2  19031  isnsg4  19042  cycsubmel  19072  efgcpbllemb  19618  dmdprd  19863  dprdval  19868  dprdw  19875  dprd2d2  19909  dfrhm2  20246  brric2  20278  issubrg  20356  islmim  20666  lbsextlem2  20765  isdomn5  20910  cnfldfun  20949  pjfval2  21256  opsrtoslem1  21608  ntreq0  22573  cmpcov2  22886  cmpsub  22896  2ndcdisj  22952  unisngl  23023  txbas  23063  elpt  23068  txkgen  23148  xkococn  23156  fbun  23336  trfil2  23383  fin1aufil  23428  alexsubALTlem3  23545  cnextcn  23563  qustgplem  23617  eltsms  23629  ustn0  23717  fmucndlem  23788  metrest  24025  restmetu  24071  isclmp  24605  srabn  24869  ellogdm  26139  1cubr  26337  leibpilem2  26436  dmarea  26452  vmasum  26709  dchrelbas2  26730  2lgslem4  26899  nosupbnd1lem4  27204  nosupbnd2lem1  27208  slenlt  27245  madeval2  27338  made0  27358  tgcgr4  27772  ltgov  27838  axlowdimlem13  28202  axeuclidlem  28210  numedglnl  28394  nbupgrres  28611  vtxd0nedgb  28735  rusgrprc  28837  usgr2pth0  29012  wspthsnwspthsnon  29160  isclwwlk  29227  clwwlkn1  29284  clwwlkn2  29287  clwwlknonel  29338  3pthdlem1  29407  iseupthf1o  29445  frgr3v  29518  fusgr2wsp2nb  29577  frgrregord013  29638  h2hcau  30220  h2hlm  30221  shlesb1i  30627  shne0i  30689  chnlei  30726  cmbr2i  30837  pjneli  30964  ho02i  31070  adjsym  31074  adjeu  31130  lnopeqi  31249  largei  31508  atoml2i  31624  cdj3lem3b  31681  or3di  31689  mo5f  31717  dmrab  31725  disjnf  31789  disjorf  31798  ssrelf  31832  ofpreima  31878  disjdsct  31912  1stpreima  31916  2ndpreima  31917  f1od2  31934  xrdifh  31979  nndiffz1  31985  prmidl0  32558  zarclsun  32839  ordtconnlem1  32893  ind1a  33006  measiuns  33204  elunirnmbfm  33239  eulerpartlemr  33362  eulerpartlemgh  33366  eulerpartlemn  33369  ballotlemodife  33485  bnj250  33701  bnj334  33713  bnj345  33714  bnj89  33721  bnj115  33725  bnj919  33767  bnj1304  33819  bnj92  33862  bnj124  33871  bnj126  33873  bnj154  33878  bnj155  33879  bnj523  33887  bnj526  33888  bnj540  33892  bnj581  33908  bnj916  33933  bnj929  33936  bnj964  33943  bnj978  33949  bnj983  33951  bnj1039  33971  bnj1040  33972  bnj1123  33986  bnj1128  33990  bnj1398  34034  lfuhgr3  34099  cvmlift2lem1  34282  satfv0  34338  satf0  34352  satf0op  34357  satffunlem  34381  satffunlem1lem1  34382  satffunlem2lem1  34384  elmthm  34556  quad3  34644  3orit  34674  dftr6  34710  eldm3  34720  elrn3  34721  elima4  34736  19.12b  34762  brtxp  34841  brtxp2  34842  brpprod  34846  brpprod3a  34847  elfix  34864  dffix2  34866  ellimits  34871  sscoid  34874  dffun10  34875  elfuns  34876  elsingles  34879  brimg  34898  brapply  34899  brsuccf  34902  funpartlem  34903  brrestrict  34910  dfrecs2  34911  dfrdg4  34912  brlb  34916  altopthc  34932  altopthd  34933  fvtransport  34993  hfext  35144  nn0prpw  35197  filnetlem4  35255  df3nandALT2  35274  bj-sbeq  35770  bj-csbsnlem  35772  bj-elsngl  35838  bj-eltag  35847  bj-tagex  35857  bj-projun  35864  bj-reabeq  35897  bj-disj2r  35898  bj-restuni  35967  bj-elid6  36040  bj-eldiag  36046  bj-eldiag2  36047  topdifinffinlem  36217  relowlpssretop  36234  fvineqsneq  36282  wl-3xorbi  36343  wl-2mintru1  36360  wl-df3maxtru1  36362  wl-dfclab  36447  phpreu  36461  poimirlem24  36501  poimirlem26  36503  poimirlem30  36507  areacirclem5  36569  isbnd2  36640  sbcalf  36971  sbcexf  36972  sbccom2  36982  sbccom2f  36983  sbccom2fi  36984  csbcom2fi  36985  anan  37082  br1cnvinxp  37113  idinxpssinxp2  37176  ineleq  37212  brabidgaw  37223  brabidga  37224  inxpxrn  37254  rnxrn  37257  cossssid2  37327  cossssid3  37328  cosscnvssid3  37335  dfeldisj3  37578  dfeldisj4  37579  antisymrelres  37622  dfmembpart2  37629  mpet3  37695  cpet2  37696  prtlem70  37716  prtlem16  37728  ishlat2  38212  pmapglb  38630  polval2N  38766  dicelval3  40040  mapdordlem1a  40494  prjspeclsp  41351  fz1eqin  41493  7rexfrabdioph  41524  rmydioph  41739  dford4  41754  areaquad  41951  onsupmaxb  41974  onov0suclim  42010  nnoeomeqom  42048  tfsconcat0i  42081  faosnf0.11b  42164  ifpan23  42197  ifpdfnan  42223  ifpdfxor  42224  ifpidg  42228  ifpid1g  42231  ifpim123g  42237  ifp1bi  42239  ifpimimb  42241  ifpororb  42242  ifpbibib  42247  rp-fakeuninass  42253  dfsucon  42260  minregex  42271  cllem0  42303  rababg  42311  elmapintrab  42313  elmapintab  42333  undmrnresiss  42341  dfxor4  42503  dfhe3  42512  dffrege115  42715  frege131  42731  frege133  42733  clsk1indlem4  42781  clsk1indlem1  42782  expandrexn  43036  rr-groth  43044  rr-grothshortbi  43048  undisjrab  43051  pm13.196a  43159  eelT11  43454  eelTT1  43457  eelT01  43458  eel0T1  43459  uunTT1  43540  uunTT1p1  43541  uunTT1p2  43542  uunT11  43543  uunT11p1  43544  uunT11p2  43545  uun111  43552  ssrabf  43789  rabssf  43794  disjinfi  43877  elicores  44233  fourierdlem42  44852  iundjiun  45163  2reu7  45806  2reu8  45807  2reu8i  45808  dfdfat2  45823  aovov0bi  45891  afv2orxorb  45923  afv2ndeffv0  45955  ichcircshi  46109  ichan  46110  icheq  46117  ichal  46121  prpair  46156  prproropf1olem0  46157  257prm  46216  fmtno4prmfac  46227  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  uspgrsprf1  46512  opeliun2xp  46962  rrx2xpref1o  47358  isthincd2  47612  aacllem  47802