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  3695  rexrab2  3697  reu2  3722  rmo4  3727  reu8  3730  rmo3f  3731  2reu5lem3  3754  sbc3an  3848  sbcimdv  3852  reu8nf  3872  rmo2  3882  rmo3  3884  rmoanim  3889  dfss2OLD  3970  ss2rab  4069  rabss  4070  ssrab  4071  dfdif3  4115  symdifass  4252  dfss4  4259  undi  4275  indifdi  4284  undif3  4291  difin2  4292  difin0ss  4369  ab0OLD  4376  disj  4448  disjOLD  4449  disj4  4459  rabsssn  4671  disjsn  4716  snssb  4787  raldifsni  4799  ssunpr  4836  sspr  4837  sstp  4838  uni0b  4938  uni0c  4939  ssint  4969  intprg  4986  iunssf  5048  iunss  5049  iundif2  5078  disjor  5129  nfnid  5374  reusv2lem4  5400  ssextss  5454  exss  5464  eqvinop  5488  sbcop  5490  opcom  5502  opeqpr  5506  brtp  5524  brabsb  5532  opelopabf  5546  dfid3  5578  pofun  5607  opeliunxp  5744  xpiundi  5747  brinxp2  5754  reliun  5817  exopxfr  5844  cnvuni  5887  dmopab3  5920  rnep  5927  elres  6021  elsnres  6022  elrid  6046  cnvsym  6114  cnvsymOLD  6115  asymref2  6119  intirr  6120  xpeq0  6160  xpdifid  6168  ssrnres  6178  dminxp  6180  dfrel4v  6190  elid  6199  dmsnn0  6207  rnco  6252  coeq0  6255  resssxp  6270  dfpo2  6296  snres0  6298  sspred  6310  frpoind  6344  wfiOLD  6353  sb8iota  6508  dffun2OLDOLD  6556  fun11  6623  isarep1  6638  isarep1OLD  6639  dff1o4  6842  opabiota  6975  fvopab5  7031  eqfnfv3  7035  fvn0ssdmfun  7077  fnressn  7156  f13dfv  7272  dff1o6  7273  fliftel  7306  oprabidw  7440  oprabid  7441  eloprabga  7516  mpo2eqb  7541  ralrnmpo  7547  uniuni  7749  dflim3  7836  dfom2  7857  elxp4  7913  elxp5  7914  opabex3d  7952  opabex3rd  7953  opabex3  7954  el2xptp  8021  fsplit  8103  xporderlem  8113  ralxp3f  8123  frpoins3xpg  8126  poxp2  8129  suppvalbr  8150  dfrecs3  8372  dfrecs3OLD  8373  tz7.48lem  8441  seqomlem2  8451  oaord  8547  oeeu  8603  nnaord  8619  ecid  8776  mptelixpg  8929  elixpsn  8931  xpsnen  9055  xpcomco  9062  xpassen  9066  omxpenlem  9073  dom0OLD  9103  modom  9244  brttrcl2  9709  ttrcltr  9711  rnttrcl  9717  frind  9745  tz9.12lem3  9784  rankxpsuc  9877  cp  9886  cardprclem  9974  infxpenlem  10008  dfac5lem1  10118  dfac5lem2  10119  dfac5lem5  10122  dfac10c  10133  kmlem3  10147  kmlem12  10156  kmlem13  10157  kmlem14  10158  kmlem15  10159  ackbij2  10238  cf0  10246  cflim2  10258  dffin7-2  10393  dfacfin7  10394  fin1a2lem12  10406  axdc3lem3  10447  cfpwsdom  10579  recmulnq  10959  genpass  11004  psslinpr  11026  suplem2pr  11048  opelreal  11125  ltxrlt  11284  addrid  11394  elnn0  12474  elxnn0  12546  elnn0z  12571  nnwos  12899  elxr  13096  xrnepnf  13098  elfzuzb  13495  4fvwrd4  13621  preduz  13623  elfzo2  13635  ssnn0fi  13950  sqeqori  14178  xpcogend  14921  cotr2g  14923  fsumcom2  15720  modfsummod  15740  fprodcom2  15928  rpnnen2lem12  16168  gcdcllem1  16440  isprm2  16619  isprm7  16645  pythagtriplem2  16750  infpn2  16846  4sqlem12  16889  initoid  17951  termoid  17952  eldmcoa  18015  oduposb  18282  gsumwspan  18727  smndex1basss  18786  smndex1mgm  18788  isnsg2  19036  isnsg4  19047  cycsubmel  19077  efgcpbllemb  19623  dmdprd  19868  dprdval  19873  dprdw  19880  dprd2d2  19914  dfrhm2  20253  brric2  20285  issubrg  20319  islmim  20673  lbsextlem2  20772  isdomn5  20917  cnfldfun  20956  pjfval2  21264  opsrtoslem1  21616  ntreq0  22581  cmpcov2  22894  cmpsub  22904  2ndcdisj  22960  unisngl  23031  txbas  23071  elpt  23076  txkgen  23156  xkococn  23164  fbun  23344  trfil2  23391  fin1aufil  23436  alexsubALTlem3  23553  cnextcn  23571  qustgplem  23625  eltsms  23637  ustn0  23725  fmucndlem  23796  metrest  24033  restmetu  24079  isclmp  24613  srabn  24877  ellogdm  26147  1cubr  26347  leibpilem2  26446  dmarea  26462  vmasum  26719  dchrelbas2  26740  2lgslem4  26909  nosupbnd1lem4  27214  nosupbnd2lem1  27218  slenlt  27255  madeval2  27349  made0  27369  tgcgr4  27813  ltgov  27879  axlowdimlem13  28243  axeuclidlem  28251  numedglnl  28435  nbupgrres  28652  vtxd0nedgb  28776  rusgrprc  28878  usgr2pth0  29053  wspthsnwspthsnon  29201  isclwwlk  29268  clwwlkn1  29325  clwwlkn2  29328  clwwlknonel  29379  3pthdlem1  29448  iseupthf1o  29486  frgr3v  29559  fusgr2wsp2nb  29618  frgrregord013  29679  h2hcau  30263  h2hlm  30264  shlesb1i  30670  shne0i  30732  chnlei  30769  cmbr2i  30880  pjneli  31007  ho02i  31113  adjsym  31117  adjeu  31173  lnopeqi  31292  largei  31551  atoml2i  31667  cdj3lem3b  31724  or3di  31732  mo5f  31760  dmrab  31768  disjnf  31832  disjorf  31841  ssrelf  31875  ofpreima  31921  disjdsct  31955  1stpreima  31959  2ndpreima  31960  f1od2  31977  xrdifh  32022  nndiffz1  32028  prmidl0  32600  zarclsun  32881  ordtconnlem1  32935  ind1a  33048  measiuns  33246  elunirnmbfm  33281  eulerpartlemr  33404  eulerpartlemgh  33408  eulerpartlemn  33411  ballotlemodife  33527  bnj250  33743  bnj334  33755  bnj345  33756  bnj89  33763  bnj115  33767  bnj919  33809  bnj1304  33861  bnj92  33904  bnj124  33913  bnj126  33915  bnj154  33920  bnj155  33921  bnj523  33929  bnj526  33930  bnj540  33934  bnj581  33950  bnj916  33975  bnj929  33978  bnj964  33985  bnj978  33991  bnj983  33993  bnj1039  34013  bnj1040  34014  bnj1123  34028  bnj1128  34032  bnj1398  34076  lfuhgr3  34141  cvmlift2lem1  34324  satfv0  34380  satf0  34394  satf0op  34399  satffunlem  34423  satffunlem1lem1  34424  satffunlem2lem1  34426  elmthm  34598  quad3  34686  3orit  34716  dftr6  34752  eldm3  34762  elrn3  34763  elima4  34778  19.12b  34804  brtxp  34883  brtxp2  34884  brpprod  34888  brpprod3a  34889  elfix  34906  dffix2  34908  ellimits  34913  sscoid  34916  dffun10  34917  elfuns  34918  elsingles  34921  brimg  34940  brapply  34941  brsuccf  34944  funpartlem  34945  brrestrict  34952  dfrecs2  34953  dfrdg4  34954  brlb  34958  altopthc  34974  altopthd  34975  fvtransport  35035  hfext  35186  gg-cnfldfun  35228  nn0prpw  35256  filnetlem4  35314  df3nandALT2  35333  bj-sbeq  35829  bj-csbsnlem  35831  bj-elsngl  35897  bj-eltag  35906  bj-tagex  35916  bj-projun  35923  bj-reabeq  35956  bj-disj2r  35957  bj-restuni  36026  bj-elid6  36099  bj-eldiag  36105  bj-eldiag2  36106  topdifinffinlem  36276  relowlpssretop  36293  fvineqsneq  36341  wl-3xorbi  36402  wl-2mintru1  36419  wl-df3maxtru1  36421  wl-dfclab  36506  phpreu  36520  poimirlem24  36560  poimirlem26  36562  poimirlem30  36566  areacirclem5  36628  isbnd2  36699  sbcalf  37030  sbcexf  37031  sbccom2  37041  sbccom2f  37042  sbccom2fi  37043  csbcom2fi  37044  anan  37141  br1cnvinxp  37172  idinxpssinxp2  37235  ineleq  37271  brabidgaw  37282  brabidga  37283  inxpxrn  37313  rnxrn  37316  cossssid2  37386  cossssid3  37387  cosscnvssid3  37394  dfeldisj3  37637  dfeldisj4  37638  antisymrelres  37681  dfmembpart2  37688  mpet3  37754  cpet2  37755  prtlem70  37775  prtlem16  37787  ishlat2  38271  pmapglb  38689  polval2N  38825  dicelval3  40099  mapdordlem1a  40553  prjspeclsp  41402  fz1eqin  41555  7rexfrabdioph  41586  rmydioph  41801  dford4  41816  areaquad  42013  onsupmaxb  42036  onov0suclim  42072  nnoeomeqom  42110  tfsconcat0i  42143  faosnf0.11b  42226  ifpan23  42259  ifpdfnan  42285  ifpdfxor  42286  ifpidg  42290  ifpid1g  42293  ifpim123g  42299  ifp1bi  42301  ifpimimb  42303  ifpororb  42304  ifpbibib  42309  rp-fakeuninass  42315  dfsucon  42322  minregex  42333  cllem0  42365  rababg  42373  elmapintrab  42375  elmapintab  42395  undmrnresiss  42403  dfxor4  42565  dfhe3  42574  dffrege115  42777  frege131  42793  frege133  42795  clsk1indlem4  42843  clsk1indlem1  42844  expandrexn  43098  rr-groth  43106  rr-grothshortbi  43110  undisjrab  43113  pm13.196a  43221  eelT11  43516  eelTT1  43519  eelT01  43520  eel0T1  43521  uunTT1  43602  uunTT1p1  43603  uunTT1p2  43604  uunT11  43605  uunT11p1  43606  uunT11p2  43607  uun111  43614  ssrabf  43851  rabssf  43856  disjinfi  43939  elicores  44294  fourierdlem42  44913  iundjiun  45224  2reu7  45867  2reu8  45868  2reu8i  45869  dfdfat2  45884  aovov0bi  45952  afv2orxorb  45984  afv2ndeffv0  46016  ichcircshi  46170  ichan  46171  icheq  46178  ichal  46182  prpair  46217  prproropf1olem0  46218  257prm  46277  fmtno4prmfac  46288  nnsum4primeseven  46516  nnsum4primesevenALTV  46517  uspgrsprf1  46573  pzriprnglem3  46855  opeliun2xp  47056  rrx2xpref1o  47452  isthincd2  47706  aacllem  47896