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  2107  excom13  2169  sbcom2  2178  sbco4OLD  2180  sbn  2286  sbnf  2317  19.12vv  2351  eeeanv  2354  ee4anv  2355  ee4anvOLD  2356  2sb8ef  2360  sbel2x  2478  2sb8e  2534  dfmo2  2596  sb8eulem  2598  2mo2  2647  2eu7  2658  2eu8  2659  sbabel  2931  3r19.43  3105  r19.23v  3163  2ralor  3210  rexcom13  3269  cbvreu  3391  rabrabi  3418  cgsex4g  3487  ceqsex2  3493  ceqsex2v  3494  ceqsex3v  3495  ceqsex4v  3496  ceqsex6v  3497  ceqsex8v  3498  ralrab2  3656  rexrab2  3658  reu2  3683  rmo4  3688  reu8  3691  rmo3f  3692  2reu5lem3  3715  sbcimdv  3809  reu8nf  3827  rmo2  3837  rmo3  3839  rmoanim  3844  ss2rab  4021  rabss  4022  ssrab  4023  dfdif3OLD  4070  symdifass  4214  dfss4  4221  undi  4237  indifdi  4246  undif3  4252  reuun2  4277  difin0ss  4325  disj  4402  disj4  4411  rabsssn  4625  disjsn  4668  snssb  4739  raldifsni  4751  ssunpr  4790  sspr  4791  sstp  4792  uni0b  4889  uni0c  4890  ssint  4919  intprg  4936  iunssf  4998  iunssfOLD  4999  iunss  5000  iunssOLD  5001  iundif2  5029  disjor  5080  nfnid  5320  reusv2lem4  5346  ssextss  5401  exss  5411  eqvinop  5435  sbcop  5437  opcom  5449  opeqpr  5453  brtp  5471  brabsb  5479  opelopabf  5493  dfid3  5522  pofun  5550  opeliunxp  5691  opeliun2xp  5692  xpiundi  5695  brinxp2  5702  exopxfr  5792  cnvuni  5835  dmopab3  5868  rnep  5876  dmxp  5878  rnopab3  5905  elres  5979  elsnres  5980  elrid  6005  cnvsym  6071  asymref2  6074  intirr  6075  cnvopab  6094  xpeq0  6118  difxp  6122  xpdifid  6126  ssrnres  6136  dminxp  6138  dfrel4v  6148  elid  6157  dmsnn0  6165  imaco  6209  rnco  6210  rncoOLD  6211  coeq0  6214  resssxp  6228  dfpo2  6254  snres0  6256  sspred  6268  frpoind  6300  sb8iota  6459  fun11  6566  isarep1  6581  dff1o4  6782  opabiota  6916  fvopab5  6974  eqfnfv3  6978  fvn0ssdmfun  7019  fnressn  7103  f13dfv  7220  dff1o6  7221  fliftel  7255  oprabidw  7389  oprabid  7390  eloprabga  7467  mpo2eqb  7490  ralrnmpo  7497  uniuni  7707  dflim3  7789  dfom2  7810  elxp4  7864  elxp5  7865  opabex3d  7909  opabex3rd  7910  opabex3  7911  el2xptp  7979  fsplit  8059  xporderlem  8069  ralxp3f  8079  frpoins3xpg  8082  poxp2  8085  suppvalbr  8106  dfrecs3  8304  tz7.48lem  8372  seqomlem2  8382  oaord  8474  oeeu  8531  nnaord  8547  ecid  8717  mptelixpg  8873  elixpsn  8875  xpsnen  8989  xpcomco  8995  xpassen  8999  omxpenlem  9006  modom  9151  brttrcl2  9623  ttrcltr  9625  rnttrcl  9631  frind  9662  tz9.12lem3  9701  rankxpsuc  9794  cp  9803  cardprclem  9891  infxpenlem  9923  dfac5lem1  10033  dfac5lem2  10034  dfac5lem5  10037  dfac10c  10049  kmlem3  10063  kmlem12  10072  kmlem13  10073  kmlem14  10074  kmlem15  10075  ackbij2  10152  cf0  10161  cflim2  10173  dffin7-2  10308  dfacfin7  10309  fin1a2lem12  10321  axdc3lem3  10362  cfpwsdom  10495  recmulnq  10875  genpass  10920  psslinpr  10942  suplem2pr  10964  opelreal  11041  ltxrlt  11203  addrid  11313  elnn0  12403  elxnn0  12476  elnn0z  12501  nnwos  12828  elxr  13030  xrnepnf  13032  elfzuzb  13434  4fvwrd4  13564  preduz  13566  elfzo2  13578  ssnn0fi  13908  sqeqori  14137  xpcogend  14897  cotr2g  14899  fsumcom2  15697  modfsummod  15717  fprodcom2  15907  rpnnen2lem12  16150  gcdcllem1  16426  isprm2  16609  isprm7  16635  pythagtriplem2  16745  infpn2  16841  4sqlem12  16884  initoid  17925  termoid  17926  eldmcoa  17989  oduposb  18250  gsumwspan  18771  smndex1basss  18830  smndex1mgm  18832  isnsg2  19085  isnsg4  19096  cycsubmel  19129  efgcpbllemb  19684  dmdprd  19929  dprdval  19934  dprdw  19941  dprd2d2  19975  dfrhm2  20410  brric2  20439  issubrg  20504  isdomn5  20643  islmim  21014  lbsextlem2  21114  cnfldfun  21323  cnfldfunOLD  21336  pzriprnglem3  21438  pjfval2  21664  opsrtoslem1  22010  ntreq0  23021  cmpcov2  23334  cmpsub  23344  2ndcdisj  23400  unisngl  23471  txbas  23511  elpt  23516  txkgen  23596  xkococn  23604  fbun  23784  trfil2  23831  fin1aufil  23876  alexsubALTlem3  23993  cnextcn  24011  qustgplem  24065  eltsms  24077  ustn0  24165  fmucndlem  24234  metrest  24468  restmetu  24514  isclmp  25053  srabn  25316  ellogdm  26604  1cubr  26808  leibpilem2  26907  dmarea  26923  vmasum  27183  dchrelbas2  27204  2lgslem4  27373  nosupbnd1lem4  27679  nosupbnd2lem1  27683  lenlts  27720  madeval2  27829  made0  27859  oniso  28267  onsfi  28352  tgcgr4  28603  ltgov  28669  axlowdimlem13  29027  axeuclidlem  29035  numedglnl  29217  nbupgrres  29437  vtxd0nedgb  29562  rusgrprc  29664  usgr2pth0  29838  wspthsnwspthsnon  29989  isclwwlk  30059  clwwlkn1  30116  clwwlkn2  30119  clwwlknonel  30170  3pthdlem1  30239  iseupthf1o  30277  frgr3v  30350  fusgr2wsp2nb  30409  frgrregord013  30470  h2hcau  31054  h2hlm  31055  shlesb1i  31461  shne0i  31523  chnlei  31560  cmbr2i  31671  pjneli  31798  ho02i  31904  adjsym  31908  adjeu  31964  lnopeqi  32083  largei  32342  atoml2i  32458  cdj3lem3b  32515  or3di  32533  mo5f  32563  dmrab  32571  rabsspr  32576  rabsstp  32577  disjnf  32645  disjorf  32654  ssrelf  32693  ofpreima  32743  disjdsct  32782  1stpreima  32786  2ndpreima  32787  f1od2  32798  xrdifh  32860  nndiffz1  32866  ind1a  32938  domnprodeq0  33358  prmidl0  33531  zarclsun  34027  ordtconnlem1  34081  measiuns  34374  elunirnmbfm  34409  eulerpartlemr  34531  eulerpartlemgh  34535  eulerpartlemn  34538  ballotlemodife  34655  bnj250  34857  bnj334  34869  bnj345  34870  bnj89  34877  bnj115  34881  bnj919  34923  bnj1304  34975  bnj92  35018  bnj124  35027  bnj126  35029  bnj154  35034  bnj155  35035  bnj523  35043  bnj526  35044  bnj540  35048  bnj581  35064  bnj916  35089  bnj929  35092  bnj964  35099  bnj978  35105  bnj983  35107  bnj1039  35127  bnj1040  35128  bnj1123  35142  bnj1128  35146  bnj1398  35190  lfuhgr3  35314  cvmlift2lem1  35496  satfv0  35552  satf0  35566  satf0op  35571  satffunlem  35595  satffunlem1lem1  35596  satffunlem2lem1  35598  elmthm  35770  quad3  35864  3orit  35910  dftr6  35945  eldm3  35955  elrn3  35956  elima4  35970  19.12b  35993  brtxp  36072  brtxp2  36073  brpprod  36077  brpprod3a  36078  elfix  36095  dffix2  36097  ellimits  36102  sscoid  36105  dffun10  36106  elfuns  36107  elsingles  36110  brimg  36129  brapply  36130  lemsuccf  36133  brsuccf  36134  funpartlem  36136  brrestrict  36143  dfrecs2  36144  dfrdg4  36145  brlb  36149  altopthc  36165  altopthd  36166  fvtransport  36226  hfext  36377  ss-ax8  36419  nn0prpw  36517  filnetlem4  36575  df3nandALT2  36594  regsfromregtr  36668  bj-sbeq  37102  bj-csbsnlem  37104  bj-elsngl  37169  bj-eltag  37178  bj-tagex  37188  bj-projun  37195  bj-reabeq  37228  bj-disj2r  37229  bj-restuni  37302  bj-elid6  37375  bj-eldiag  37381  bj-eldiag2  37382  topdifinffinlem  37552  relowlpssretop  37569  fvineqsneq  37617  wl-3xorbi  37678  wl-2mintru1  37695  wl-df3maxtru1  37697  wl-dfclab  37790  phpreu  37805  poimirlem24  37845  poimirlem26  37847  poimirlem30  37851  areacirclem5  37913  isbnd2  37984  sbcalf  38315  sbcexf  38316  sbccom2  38326  sbccom2f  38327  sbccom2fi  38328  csbcom2fi  38329  anan  38431  br1cnvinxp  38454  idinxpssinxp2  38517  ineleq  38547  brabidgaw  38558  brabidga  38559  inxpxrn  38603  rnxrn  38606  dfsucmap3  38637  cossssid2  38731  cossssid3  38732  cosscnvssid3  38739  dfeldisj3  38978  dfeldisj4  38979  antisymrelres  39022  dfmembpart2  39029  mpet3  39095  cpet2  39096  prtlem70  39117  prtlem16  39129  ishlat2  39613  pmapglb  40030  polval2N  40166  dicelval3  41440  mapdordlem1a  41894  redvmptabs  42615  fimgmcyclem  42788  fimgmcyc  42789  prjspeclsp  42855  sn-isghm  42916  abbibw  42920  fz1eqin  43011  7rexfrabdioph  43042  rmydioph  43256  dford4  43271  areaquad  43458  onsupmaxb  43481  onov0suclim  43516  nnoeomeqom  43554  tfsconcat0i  43587  faosnf0.11b  43668  ifpan23  43701  ifpdfnan  43727  ifpdfxor  43728  ifpidg  43732  ifpid1g  43735  ifpim123g  43741  ifp1bi  43743  ifpimimb  43745  ifpororb  43746  ifpbibib  43751  rp-fakeuninass  43757  dfsucon  43764  minregex  43775  cllem0  43807  rababg  43815  elmapintrab  43817  elmapintab  43837  undmrnresiss  43845  dfxor4  44007  dfhe3  44016  dffrege115  44219  frege131  44235  frege133  44237  clsk1indlem4  44285  clsk1indlem1  44286  expandrexn  44532  rr-groth  44540  rr-grothshortbi  44544  undisjrab  44547  pm13.196a  44655  eelT11  44947  eelTT1  44950  eelT01  44951  eel0T1  44952  uunTT1  45033  uunTT1p1  45034  uunTT1p2  45035  uunT11  45036  uunT11p1  45037  uunT11p2  45038  uun111  45045  xpwf  45205  permaxinf2lem  45253  permac8prim  45255  ssrabf  45358  rabssf  45363  disjinfi  45436  elicores  45779  fourierdlem42  46393  iundjiun  46704  2reu7  47357  2reu8  47358  2reu8i  47359  dfdfat2  47374  aovov0bi  47442  afv2orxorb  47474  afv2ndeffv0  47506  ichcircshi  47700  ichan  47701  icheq  47708  ichal  47712  prpair  47747  prproropf1olem0  47748  257prm  47807  fmtno4prmfac  47818  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  clnbgrel  48074  isubgr3stgrlem4  48215  usgrexmpl2nb1  48278  usgrexmpl2nb2  48279  gpgprismgr4cycllem10  48350  uspgrsprf1  48393  rrx2xpref1o  48964  iinxp  49076  resinsn  49117  resinsnALT  49118  0funcALT  49333  catcsect  49643  isthincd2  49682  aacllem  50046