Theorem 3bitri 299

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  bibi1i  340  pm5.32  581  biadan  828  orbi1i  924  orass  932  or32  936  cases  1053  dn1  1068  3anidm  1115  an33rean  1503  nanbi  1519  excxor  1535  cadan  1628  cadcomb  1632  nic-axALT  1693  tbw-bijust  1717  rb-bijust  1768  nf2  1804  19.43  1901  19.43OLD  1902  3exdistr  1979  19.12vvv  2013  sbco4  2135  excom13  2197  sbcom2  2205  sbco4OLD  2207  sbn  2313  sbnf  2344  19.12vv  2377  eeeanv  2380  ee4anv  2381  ee4anvOLD  2382  2sb8ef  2386  sbel2x  2504  2sb8e  2560  dfmo2  2622  sb8eulem  2624  2mo2  2673  2eu7  2683  2eu8  2684  sbabel  2955  3r19.43  3130  r19.23v  3188  2ralor  3235  rexcom13  3294  cbvreu  3405  rabrabi  3432  cgsex4g  3499  ceqsex2  3503  ceqsex2v  3504  ceqsex3v  3505  ceqsex4v  3506  ceqsex6v  3507  ceqsex8v  3508  ralrab2  3659  rexrab2  3661  reu2  3686  rmo4  3691  reu8  3694  rmo3f  3695  2reu5lem3  3718  sbcimdv  3810  reu8nf  3828  rmo2  3838  rmo3  3840  rmoanim  3845  ss2rab  4020  rabss  4021  ssrab  4022  dfdif3OLD  4070  symdifass  4212  dfss4  4219  undi  4235  indifdi  4244  undif3  4250  reuun2  4275  difin0ss  4323  disj  4401  disj4  4410  rabsssn  4624  disjsn  4667  snssb  4738  raldifsni  4752  ssunpr  4789  sspr  4790  sstp  4791  uni0b  4889  uni0c  4890  ssint  4919  intprg  4936  iunssf  4997  iunssfOLD  4998  iunss  4999  iunssOLD  5000  iundif2  5028  disjor  5079  nfnid  5329  reusv2lem4  5355  ssextss  5417  exss  5427  eqvinop  5452  sbcop  5454  opcom  5467  opeqpr  5471  brtp  5490  brabsb  5498  opelopabf  5512  dfid3  5541  pofun  5569  opeliunxp  5710  opeliun2xp  5711  xpiundi  5714  brinxp2  5721  exopxfr  5811  cnvuni  5858  dmopab3  5891  rnep  5899  dmxp  5901  rnopab3  5928  elres  6002  elsnres  6003  elrid  6030  cnvsym  6096  asymref2  6099  intirr  6100  cnvopab  6119  xpeq0  6140  difxp  6144  xpdifid  6148  ssrnres  6158  dminxp  6160  dfrel4v  6170  elid  6180  dmsnn0  6188  imaco  6232  rnco  6233  rncoOLD  6234  coeq0  6237  resssxp  6251  dfpo2  6277  snres0  6279  sspred  6291  frpoind  6323  sb8iota  6482  fun11  6589  isarep1  6604  dff1o4  6809  opabiota  6943  fvopab5  7003  eqfnfv3  7007  fvn0ssdmfun  7049  fnressn  7135  f13dfv  7252  dff1o6  7253  fliftel  7287  oprabidw  7421  oprabid  7422  eloprabga  7499  mpo2eqb  7522  ralrnmpo  7529  uniuni  7739  dflim3  7821  dfom2  7842  elxp4  7897  elxp5  7898  opabex3d  7940  opabex3rd  7941  opabex3  7942  el2xptp  8010  fsplit  8089  xporderlem  8100  ralxp3f  8110  frpoins3xpg  8113  poxp2  8116  suppvalbr  8137  dfrecs3  8336  tz7.48lem  8405  seqomlem2  8415  oaord  8509  oeeu  8566  nnaord  8582  ecid  8755  mptelixpg  8910  elixpsn  8912  xpsnen  9026  xpcomco  9032  xpassen  9036  omxpenlem  9043  modom  9188  brttrcl2  9662  ttrcltr  9664  rnttrcl  9670  frind  9701  tz9.12lem3  9740  rankxpsuc  9833  cp  9842  cardprclem  9930  infxpenlem  9962  dfac5lem1  10072  dfac5lem2  10073  dfac5lem5  10076  dfac10c  10088  kmlem3  10102  kmlem12  10111  kmlem13  10112  kmlem14  10113  kmlem15  10114  ackbij2  10191  cf0  10200  cflim2  10213  dffin7-2  10348  dfacfin7  10349  fin1a2lem12  10361  axdc3lem3  10402  cfpwsdom  10535  recmulnq  10915  genpass  10960  psslinpr  10982  suplem2pr  11004  opelreal  11081  ltxrlt  11246  addrid  11356  ind1a  12199  elnn0  12476  elxnn0  12549  elnn0z  12574  nnwos  12909  elxr  13111  xrnepnf  13113  elfzuzb  13516  4fvwrd4  13646  preduz  13648  elfzo2  13660  ssnn0fi  13991  sqeqori  14220  xpcogend  14980  cotr2g  14982  fsumcom2  15791  modfsummod  15812  fprodcom2  16004  rpnnen2lem12  16247  gcdcllem1  16523  isprm2  16706  isprm7  16733  pythagtriplem2  16843  infpn2  16939  4sqlem12  16982  initoid  18024  termoid  18025  eldmcoa  18088  oduposb  18349  gsumwspan  18870  smndex1basss  18932  smndex1mgm  18934  isnsg2  19187  isnsg4  19198  cycsubmel  19231  efgcpbllemb  19785  dmdprd  20030  dprdval  20035  dprdw  20042  dprd2d2  20076  dfrhm2  20509  brric2  20542  issubrg  20607  isdomn5  20746  islmim  21116  lbsextlem2  21216  cnfldfun  21425  pzriprnglem3  21522  pjfval2  21748  opsrtoslem1  22095  ntreq0  23124  cmpcov2  23437  cmpsub  23447  2ndcdisj  23503  unisngl  23574  txbas  23614  elpt  23619  txkgen  23699  xkococn  23707  fbun  23887  trfil2  23934  fin1aufil  23979  alexsubALTlem3  24096  cnextcn  24114  qustgplem  24168  eltsms  24180  ustn0  24268  fmucndlem  24337  metrest  24571  restmetu  24617  isclmp  25146  srabn  25409  ellogdm  26691  1cubr  26894  leibpilem2  26993  dmarea  27009  vmasum  27267  dchrelbas2  27288  2lgslem4  27457  nosupbnd1lem4  27762  nosupbnd2lem1  27766  lenlts  27803  madeval2  27913  made0  27943  oniso  28351  onsfi  28436  tgcgr4  28687  ltgov  28753  axlowdimlem13  29111  axeuclidlem  29119  numedglnl  29301  nbupgrres  29521  vtxd0nedgb  29645  rusgrprc  29747  usgr2pth0  29921  wspthsnwspthsnon  30072  isclwwlk  30142  clwwlkn1  30199  clwwlkn2  30202  clwwlknonel  30253  3pthdlem1  30322  iseupthf1o  30360  frgr3v  30433  fusgr2wsp2nb  30492  frgrregord013  30553  h2hcau  31138  h2hlm  31139  shlesb1i  31545  shne0i  31607  chnlei  31644  cmbr2i  31755  pjneli  31882  ho02i  31988  adjsym  31992  adjeu  32048  lnopeqi  32167  largei  32426  atoml2i  32542  cdj3lem3b  32599  or3di  32616  mo5f  32646  dmrab  32654  rabsspr  32659  rabsstp  32660  disjnf  32729  disjorf  32738  ssrelf  32777  ofpreima  32827  disjdsct  32865  1stpreima  32869  2ndpreima  32870  f1od2  32881  xrdifh  32942  nndiffz1  32948  domnprodeq0  33420  prmidl0  33597  zarclsun  34127  ordtconnlem1  34181  measiuns  34474  elunirnmbfm  34509  eulerpartlemr  34631  eulerpartlemgh  34635  eulerpartlemn  34638  ballotlemodife  34755  bnj250  34957  bnj334  34969  bnj345  34970  bnj89  34977  bnj115  34981  bnj919  35023  bnj1304  35074  bnj92  35117  bnj124  35126  bnj126  35128  bnj154  35133  bnj155  35134  bnj523  35142  bnj526  35143  bnj540  35147  bnj581  35163  bnj916  35188  bnj929  35191  bnj964  35198  bnj978  35204  bnj983  35206  bnj1039  35226  bnj1040  35227  bnj1123  35241  bnj1128  35245  bnj1398  35289  lfuhgr3  35430  cvmlift2lem1  35612  satfv0  35668  satf0  35682  satf0op  35687  satffunlem  35711  satffunlem1lem1  35712  satffunlem2lem1  35714  elmthm  35886  quad3  35980  3orit  36026  dftr6  36061  eldm3  36071  elrn3  36072  elima4  36086  19.12b  36109  brtxp  36188  brtxp2  36189  brpprod  36193  brpprod3a  36194  elfix  36211  dffix2  36213  ellimits  36218  sscoid  36221  dffun10  36222  elfuns  36223  elsingles  36226  brimg  36245  brapply  36246  lemsuccf  36249  brsuccf  36250  funpartlem  36252  brrestrict  36259  dfrecs2  36260  dfrdg4  36261  brlb  36265  altopthc  36281  altopthd  36282  fvtransport  36342  hfext  36493  ss-ax8  36545  nn0prpw  36643  filnetlem4  36701  df3nandALT2  36720  regsfromregtco  36858  mh-prprimbi  36863  mh-regprimbi  36865  mh-infprim2bi  36867  mh-infprim3bi  36868  bj-sbeq  37346  bj-csbsnlem  37348  bj-elsngl  37413  bj-eltag  37422  bj-tagex  37432  bj-projun  37439  bj-reabeq  37472  bj-disj2r  37473  bj-axseprep  37519  bj-restuni  37547  bj-elid6  37622  bj-eldiag  37628  bj-eldiag2  37629  topdifinffinlem  37801  relowlpssretop  37818  fvineqsneq  37866  wl-3xorbi  37927  wl-2mintru1  37944  wl-df3maxtru1  37946  wl-dfclab  38048  phpreu  38063  poimirlem24  38103  poimirlem26  38105  poimirlem30  38109  areacirclem5  38171  isbnd2  38242  sbcalf  38573  sbcexf  38574  sbccom2  38584  sbccom2f  38585  sbccom2fi  38586  csbcom2fi  38587  anan  38694  br1cnvinxp  38718  idinxpssinxp2  38783  ineleq  38813  brabidgaw  38832  brabidga  38833  inxpxrn  38877  rnxrn  38880  dfsucmap3  38922  cossssid2  39017  cossssid3  39018  cosscnvssid3  39025  dfeldisj3  39270  dfeldisj4  39271  antisymrelres  39325  dfmembpart2  39332  mpet3  39409  cpet2  39410  prtlem70  39441  prtlem16  39453  ishlat2  39937  pmapglb  40354  polval2N  40490  dicelval3  41764  mapdordlem1a  42218  redvmptabs  42929  fimgmcyclem  43111  fimgmcyc  43112  prjspeclsp  43154  sn-isghm  43215  abbibw  43219  fz1eqin  43310  7rexfrabdioph  43337  rmydioph  43551  dford4  43566  areaquad  43753  onsupmaxb  43776  onov0suclim  43811  nnoeomeqom  43849  tfsconcat0i  43882  faosnf0.11b  43963  ifpan23  43996  ifpdfnan  44022  ifpdfxor  44023  ifpidg  44027  ifpid1g  44030  ifpim123g  44036  ifp1bi  44038  ifpimimb  44040  ifpororb  44041  ifpbibib  44046  rp-fakeuninass  44052  dfsucon  44059  minregex  44070  cllem0  44102  rababg  44110  elmapintrab  44112  elmapintab  44132  undmrnresiss  44140  dfxor4  44302  dfhe3  44311  dffrege115  44514  frege131  44530  frege133  44532  clsk1indlem4  44580  clsk1indlem1  44581  expandrexn  44827  rr-groth  44835  rr-grothshortbi  44839  undisjrab  44842  pm13.196a  44950  eelT11  45242  eelTT1  45245  eelT01  45246  eel0T1  45247  uunTT1  45328  uunTT1p1  45329  uunTT1p2  45330  uunT11  45331  uunT11p1  45332  uunT11p2  45333  uun111  45340  xpwf  45500  permaxinf2lem  45548  permac8prim  45550  ssrabf  45652  rabssf  45657  disjinfi  45730  elicores  46069  fourierdlem42  46683  iundjiun  46994  2reu7  47665  2reu8  47666  2reu8i  47667  dfdfat2  47682  aovov0bi  47750  afv2orxorb  47782  afv2ndeffv0  47814  ichcircshi  48020  ichan  48021  icheq  48028  ichal  48032  prpair  48067  prproropf1olem0  48068  257prm  48130  fmtno4prmfac  48141  nnsum4primeseven  48382  nnsum4primesevenALTV  48383  clnbgrel  48410  isubgr3stgrlem4  48551  usgrexmpl2nb1  48614  usgrexmpl2nb2  48615  gpgprismgr4cycllem10  48686  uspgrsprf1  48729  rrx2xpref1o  49300  iinxp  49412  resinsn  49453  resinsnALT  49454  0funcALT  49669  catcsect  49979  isthincd2  50018  aacllem  50382