Theorem 3bitri 289

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

Syntax hints:   ↔ wb 198

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 199

This theorem is referenced by:  bibi1i  331  pm5.32  566  an32  633  biadan  806  biadanOLD  807  orbi1i  897  orass  905  or32  909  cases  1023  an3andi  1461  an33rean  1462  nanbi  1475  nanassOLD  1487  excxor  1493  cadan  1572  cadcomb  1576  nic-axALT  1637  tbw-bijust  1661  rb-bijust  1712  nf2  1748  19.43  1845  19.43OLD  1846  3exdistr  1920  19.12vvv  1945  sb3an  2032  equsb3rOLD  2047  excom13  2100  sbn  2214  19.12vv  2281  eeeanv  2284  ee4anv  2285  2sb8ev  2288  2sb8evOLD  2289  sbcom2  2410  sbcom2OLD  2411  sbco4  2413  sbel2x  2421  sbnOLD  2462  2sb8e  2503  sbnALT  2522  eu6  2590  eu6OLDOLD  2593  dfmo  2614  moeuOLD  2617  sb8eulem  2632  2mo2  2679  2eu7  2690  2eu8  2691  euaeOLD  2693  r19.26-3  3123  r19.23v  3225  rexcom  3297  ralcom13  3301  rexcom13  3302  cbvreu  3382  ceqsralt  3450  ceqsex2  3465  ceqsex2v  3466  ceqsex4v  3468  ralrab2  3606  rexrab2  3608  reu2  3629  rmo4  3634  reu8  3637  rmo3f  3638  2reu5lem3  3658  sbc3an  3742  reu8nf  3764  rmo2  3774  rmo3  3776  rmo3OLD  3777  rmoanim  3782  dfss2  3847  ss2rab  3938  rabss  3939  ssrab  3940  dfdif3  3982  symdifass  4116  dfss4  4123  undi  4139  undif3  4153  difin2  4154  dfnul2OLD  4182  difin0ss  4215  disj  4282  disj4  4291  rabsssn  4479  disjsn  4521  raldifsni  4602  ssunpr  4639  sspr  4640  sstp  4641  uni0b  4737  uni0c  4738  ssint  4765  iunss  4835  iundif2  4862  disjor  4911  nfnid  5129  reusv2lem4  5155  ssextss  5203  exss  5212  eqvinop  5235  sbcop  5237  opcom  5247  opeqpr  5251  brabsb  5272  opelopabf  5286  dfid3  5313  pofun  5343  opeliunxp  5469  xpiundi  5472  brinxp2  5479  reliun  5539  exopxfr  5564  cnvuni  5607  dmopab3  5635  elres  5736  elsnres  5737  elrid  5758  asymref2  5817  intirr  5818  xpeq0  5857  xpdifid  5865  ssrnres  5875  dminxp  5877  dfrel4v  5887  elid  5895  dmsnn0  5903  rnco  5944  coeq0  5947  sspred  5994  wfi  6019  sb8iota  6159  dffun2  6198  fun11  6261  isarep1  6275  dff1o4  6452  opabiota  6574  fvopab5  6625  eqfnfv3  6629  fvn0ssdmfun  6667  fnressn  6743  f13dfv  6856  dff1o6  6857  fliftel  6885  oprabid  7007  mpo2eqb  7099  ralrnmpo  7105  uniuni  7301  dflim3  7378  dfom2  7398  elxp4  7442  elxp5  7443  opabex3d  7478  opabex3rd  7479  opabex3  7480  el2xptp  7547  xporderlem  7626  dfrecs3  7813  tz7.48lem  7880  seqomlem2  7890  oaord  7974  oeeu  8030  nnaord  8046  ecid  8162  mptelixpg  8296  elixpsn  8298  xpsnen  8397  xpcomco  8403  xpassen  8407  omxpenlem  8414  dom0  8441  modom  8514  tz9.12lem3  9012  rankxpsuc  9105  cp  9114  cardprclem  9202  infxpenlem  9233  dfac5lem1  9343  dfac5lem2  9344  dfac5lem5  9347  dfac10c  9358  kmlem3  9372  kmlem12  9381  kmlem13  9382  kmlem14  9383  kmlem15  9384  ackbij2  9463  cf0  9471  cflim2  9483  dffin7-2  9618  dfacfin7  9619  fin1a2lem12  9631  axdc3lem3  9672  cfpwsdom  9804  recmulnq  10184  genpass  10229  psslinpr  10251  suplem2pr  10273  opelreal  10350  ltxrlt  10511  addid1  10620  fimaxreOLD  11386  elnn0  11709  elxnn0  11781  elnn0z  11806  nnwos  12129  elxr  12328  xrnepnf  12330  elfzuzb  12718  4fvwrd4  12843  preduz  12845  elfzo2  12857  ssnn0fi  13168  sqeqori  13391  xpcogend  14195  cotr2g  14197  fsumcom2  14989  modfsummod  15009  fprodcom2  15198  rpnnen2lem12  15438  gcdcllem1  15708  isprm2  15882  isprm7  15908  pythagtriplem2  16010  infpn2  16105  4sqlem12  16148  initoid  17123  termoid  17124  eldmcoa  17183  oduposb  17604  gsumwspan  17852  isnsg2  18093  isnsg4  18106  efgcpbllemb  18641  dmdprd  18870  dprdval  18875  dprdw  18882  dprd2d2  18916  dfrhm2  19192  brric2  19223  issubrg  19258  islmim  19556  lbsextlem2  19653  opsrtoslem1  19977  cnfldfunALT  20260  pjfval2  20555  ntreq0  21389  cmpcov2  21702  cmpsub  21712  2ndcdisj  21768  unisngl  21839  txbas  21879  elpt  21884  txkgen  21964  xkococn  21972  fbun  22152  trfil2  22199  fin1aufil  22244  alexsubALTlem3  22361  cnextcn  22379  qustgplem  22432  eltsms  22444  ustn0  22532  fmucndlem  22603  metrest  22837  restmetu  22883  isclmp  23404  srabn  23666  ellogdm  24923  1cubr  25121  leibpilem2  25221  dmarea  25237  vmasum  25494  dchrelbas2  25515  2lgslem4  25684  tgcgr4  26019  ltgov  26085  axlowdimlem13  26443  axeuclidlem  26451  numedglnl  26632  nbupgrres  26849  vtxd0nedgb  26973  rusgrprc  27075  usgr2pth0  27254  wspthsnwspthsnon  27422  isclwwlk  27490  clwwlkn1  27557  clwwlkn2  27560  clwwlknonel  27623  3pthdlem1  27693  iseupthf1o  27731  frgr3v  27809  fusgr2wsp2nb  27868  frgrregord013  27952  h2hcau  28535  h2hlm  28536  shlesb1i  28944  shne0i  29006  chnlei  29043  cmbr2i  29154  pjneli  29281  ho02i  29387  adjsym  29391  adjeu  29447  lnopeqi  29566  largei  29825  atoml2i  29941  cdj3lem3b  29998  or3di  30006  mo5f  30035  dmrab  30039  disjnf  30087  disjorf  30095  ssrelf  30130  ofpreima  30172  disjdsct  30190  1stpreima  30194  2ndpreima  30195  f1od2  30209  xrdifh  30255  nndiffz1  30261  ordtconnlem1  30808  ind1a  30919  measiuns  31118  elunirnmbfm  31153  eulerpartlemr  31274  eulerpartlemgh  31278  eulerpartlemn  31281  ballotlemodife  31398  bnj250  31616  bnj334  31628  bnj345  31629  bnj89  31636  bnj115  31640  bnj919  31683  bnj1304  31736  bnj92  31778  bnj124  31787  bnj126  31789  bnj154  31794  bnj155  31795  bnj523  31803  bnj526  31804  bnj540  31808  bnj581  31824  bnj916  31849  bnj929  31852  bnj964  31859  bnj978  31865  bnj983  31867  bnj1039  31885  bnj1040  31886  bnj1123  31900  bnj1128  31904  bnj1398  31948  cvmlift2lem1  32131  satf0  32179  satf0op  32184  elmthm  32340  quad3  32430  3orit  32462  brtp  32502  dftr6  32503  dfpo2  32508  eldm3  32514  elrn3  32515  elima4  32536  19.12b  32564  frpoind  32598  frind  32603  nosupbnd1lem4  32729  nosupbnd2lem1  32733  slenlt  32749  madeval2  32808  brtxp  32859  brtxp2  32860  brpprod  32864  brpprod3a  32865  elfix  32882  dffix2  32884  ellimits  32889  sscoid  32892  dffun10  32893  elfuns  32894  elsingles  32897  brimg  32916  brapply  32917  brsuccf  32920  funpartlem  32921  brrestrict  32928  dfrecs2  32929  dfrdg4  32930  brlb  32934  altopthc  32950  altopthd  32951  fvtransport  33011  hfext  33162  nn0prpw  33189  filnetlem4  33247  df3nandALT2  33266  bj-sbeq  33707  bj-csbsnlem  33709  bj-elsngl  33795  bj-eltag  33804  bj-tagex  33814  bj-projun  33821  bj-disj2r  33852  bj-restuni  33895  bj-eldiag  33942  bj-eldiag2  33943  topdifinffinlem  34067  relowlpssretop  34084  fvineqsneq  34131  wl-dfclab  34266  wl-dfrexsb  34289  phpreu  34314  poimirlem24  34354  poimirlem26  34356  poimirlem30  34360  areacirclem5  34424  isbnd2  34500  sbcalf  34833  sbcexf  34834  sbccom2  34844  sbccom2f  34845  sbccom2fi  34846  csbcom2fi  34847  anan  34940  idinxpssinxp2  35016  ineleq  35051  brabidga  35060  inxpxrn  35085  rnxrn  35088  cossssid2  35150  cossssid3  35151  cosscnvssid3  35158  dfeldisj3  35394  dfeldisj4  35395  prtlem70  35435  prtlem16  35447  ishlat2  35931  polval2N  36484  dicelval3  37758  mapdordlem1a  38212  prjspeclsp  38666  fz1eqin  38758  7rexfrabdioph  38790  rmydioph  39004  dford4  39019  areaquad  39216  ifpan23  39218  ifpdfnan  39245  ifpdfxor  39246  ifpidg  39250  ifpid1g  39253  ifpim123g  39259  ifp1bi  39261  ifpimimb  39263  ifpororb  39264  ifpbibib  39269  rp-fakeuninass  39275  cllem0  39284  rababg  39292  elmapintrab  39295  elmapintab  39315  undmrnresiss  39323  ss2iundf  39364  dfxor4  39471  rp-imass  39477  dfhe3  39481  dffrege115  39684  frege131  39700  frege133  39702  clsk1indlem4  39754  clsk1indlem1  39755  expandrexn  39999  rr-groth  40007  undisjrab  40051  pm13.196a  40160  eelT11  40457  eelTT1  40460  eelT01  40461  eel0T1  40462  uunTT1  40543  uunTT1p1  40544  uunTT1p2  40545  uunT11  40546  uunT11p1  40547  uunT11p2  40548  uun111  40555  iunssf  40771  ssrabf  40802  rabssf  40806  disjinfi  40876  elicores  41238  fourierdlem42  41863  iundjiun  42171  2reu7  42714  2reu8  42715  2reu8i  42716  dfdfat2  42731  aovov0bi  42799  afv2orxorb  42831  afv2ndeffv0  42863  ichcircshi  42980  icheq  42988  ichal  42995  prpair  43029  prproropf1olem0  43030  257prm  43089  fmtno4prmfac  43100  nnsum4primeseven  43331  nnsum4primesevenALTV  43332  uspgrsprf1  43388  opeliun2xp  43743  rrx2xpref1o  44071  aacllem  44267