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  819  orbi1i  914  orass  922  or32  926  cases  1043  dn1  1058  3anidm  1104  an33rean  1486  nanbi  1502  excxor  1518  cadan  1611  cadcomb  1615  nic-axALT  1676  tbw-bijust  1700  rb-bijust  1751  nf2  1787  19.43  1884  19.43OLD  1885  3exdistr  1962  19.12vvv  1996  sbco4  2108  excom13  2170  sbcom2  2179  sbco4OLD  2181  sbn  2287  sbnf  2318  19.12vv  2352  eeeanv  2355  ee4anv  2356  ee4anvOLD  2357  2sb8ef  2361  sbel2x  2479  2sb8e  2535  dfmo2  2597  sb8eulem  2599  2mo2  2648  2eu7  2659  2eu8  2660  sbabel  2932  3r19.43  3107  r19.23v  3165  2ralor  3212  rexcom13  3271  cbvreu  3393  rabrabi  3420  cgsex4g  3489  ceqsex2  3495  ceqsex2v  3496  ceqsex3v  3497  ceqsex4v  3498  ceqsex6v  3499  ceqsex8v  3500  ralrab2  3658  rexrab2  3660  reu2  3685  rmo4  3690  reu8  3693  rmo3f  3694  2reu5lem3  3717  sbcimdv  3811  reu8nf  3829  rmo2  3839  rmo3  3841  rmoanim  3846  ss2rab  4023  rabss  4024  ssrab  4025  dfdif3OLD  4072  symdifass  4216  dfss4  4223  undi  4239  indifdi  4248  undif3  4254  reuun2  4279  difin0ss  4327  disj  4404  disj4  4413  rabsssn  4627  disjsn  4670  snssb  4741  raldifsni  4753  ssunpr  4792  sspr  4793  sstp  4794  uni0b  4891  uni0c  4892  ssint  4921  intprg  4938  iunssf  5000  iunssfOLD  5001  iunss  5002  iunssOLD  5003  iundif2  5031  disjor  5082  nfnid  5322  reusv2lem4  5348  ssextss  5408  exss  5418  eqvinop  5443  sbcop  5445  opcom  5457  opeqpr  5461  brtp  5479  brabsb  5487  opelopabf  5501  dfid3  5530  pofun  5558  opeliunxp  5699  opeliun2xp  5700  xpiundi  5703  brinxp2  5710  exopxfr  5800  cnvuni  5843  dmopab3  5876  rnep  5884  dmxp  5886  rnopab3  5913  elres  5987  elsnres  5988  elrid  6013  cnvsym  6079  asymref2  6082  intirr  6083  cnvopab  6102  xpeq0  6126  difxp  6130  xpdifid  6134  ssrnres  6144  dminxp  6146  dfrel4v  6156  elid  6165  dmsnn0  6173  imaco  6217  rnco  6218  rncoOLD  6219  coeq0  6222  resssxp  6236  dfpo2  6262  snres0  6264  sspred  6276  frpoind  6308  sb8iota  6467  fun11  6574  isarep1  6589  dff1o4  6790  opabiota  6924  fvopab5  6983  eqfnfv3  6987  fvn0ssdmfun  7028  fnressn  7113  f13dfv  7230  dff1o6  7231  fliftel  7265  oprabidw  7399  oprabid  7400  eloprabga  7477  mpo2eqb  7500  ralrnmpo  7507  uniuni  7717  dflim3  7799  dfom2  7820  elxp4  7874  elxp5  7875  opabex3d  7919  opabex3rd  7920  opabex3  7921  el2xptp  7989  fsplit  8069  xporderlem  8079  ralxp3f  8089  frpoins3xpg  8092  poxp2  8095  suppvalbr  8116  dfrecs3  8314  tz7.48lem  8382  seqomlem2  8392  oaord  8484  oeeu  8541  nnaord  8557  ecid  8729  mptelixpg  8885  elixpsn  8887  xpsnen  9001  xpcomco  9007  xpassen  9011  omxpenlem  9018  modom  9163  brttrcl2  9635  ttrcltr  9637  rnttrcl  9643  frind  9674  tz9.12lem3  9713  rankxpsuc  9806  cp  9815  cardprclem  9903  infxpenlem  9935  dfac5lem1  10045  dfac5lem2  10046  dfac5lem5  10049  dfac10c  10061  kmlem3  10075  kmlem12  10084  kmlem13  10085  kmlem14  10086  kmlem15  10087  ackbij2  10164  cf0  10173  cflim2  10185  dffin7-2  10320  dfacfin7  10321  fin1a2lem12  10333  axdc3lem3  10374  cfpwsdom  10507  recmulnq  10887  genpass  10932  psslinpr  10954  suplem2pr  10976  opelreal  11053  ltxrlt  11215  addrid  11325  elnn0  12415  elxnn0  12488  elnn0z  12513  nnwos  12840  elxr  13042  xrnepnf  13044  elfzuzb  13446  4fvwrd4  13576  preduz  13578  elfzo2  13590  ssnn0fi  13920  sqeqori  14149  xpcogend  14909  cotr2g  14911  fsumcom2  15709  modfsummod  15729  fprodcom2  15919  rpnnen2lem12  16162  gcdcllem1  16438  isprm2  16621  isprm7  16647  pythagtriplem2  16757  infpn2  16853  4sqlem12  16896  initoid  17937  termoid  17938  eldmcoa  18001  oduposb  18262  gsumwspan  18783  smndex1basss  18842  smndex1mgm  18844  isnsg2  19097  isnsg4  19108  cycsubmel  19141  efgcpbllemb  19696  dmdprd  19941  dprdval  19946  dprdw  19953  dprd2d2  19987  dfrhm2  20422  brric2  20451  issubrg  20516  isdomn5  20655  islmim  21026  lbsextlem2  21126  cnfldfun  21335  cnfldfunOLD  21348  pzriprnglem3  21450  pjfval2  21676  opsrtoslem1  22022  ntreq0  23033  cmpcov2  23346  cmpsub  23356  2ndcdisj  23412  unisngl  23483  txbas  23523  elpt  23528  txkgen  23608  xkococn  23616  fbun  23796  trfil2  23843  fin1aufil  23888  alexsubALTlem3  24005  cnextcn  24023  qustgplem  24077  eltsms  24089  ustn0  24177  fmucndlem  24246  metrest  24480  restmetu  24526  isclmp  25065  srabn  25328  ellogdm  26616  1cubr  26820  leibpilem2  26919  dmarea  26935  vmasum  27195  dchrelbas2  27216  2lgslem4  27385  nosupbnd1lem4  27691  nosupbnd2lem1  27695  lenlts  27732  madeval2  27841  made0  27871  oniso  28279  onsfi  28364  tgcgr4  28615  ltgov  28681  axlowdimlem13  29039  axeuclidlem  29047  numedglnl  29229  nbupgrres  29449  vtxd0nedgb  29574  rusgrprc  29676  usgr2pth0  29850  wspthsnwspthsnon  30001  isclwwlk  30071  clwwlkn1  30128  clwwlkn2  30131  clwwlknonel  30182  3pthdlem1  30251  iseupthf1o  30289  frgr3v  30362  fusgr2wsp2nb  30421  frgrregord013  30482  h2hcau  31066  h2hlm  31067  shlesb1i  31473  shne0i  31535  chnlei  31572  cmbr2i  31683  pjneli  31810  ho02i  31916  adjsym  31920  adjeu  31976  lnopeqi  32095  largei  32354  atoml2i  32470  cdj3lem3b  32527  or3di  32544  mo5f  32574  dmrab  32582  rabsspr  32587  rabsstp  32588  disjnf  32656  disjorf  32665  ssrelf  32704  ofpreima  32754  disjdsct  32792  1stpreima  32796  2ndpreima  32797  f1od2  32808  xrdifh  32870  nndiffz1  32876  ind1a  32948  domnprodeq0  33369  prmidl0  33542  zarclsun  34047  ordtconnlem1  34101  measiuns  34394  elunirnmbfm  34429  eulerpartlemr  34551  eulerpartlemgh  34555  eulerpartlemn  34558  ballotlemodife  34675  bnj250  34877  bnj334  34889  bnj345  34890  bnj89  34897  bnj115  34901  bnj919  34943  bnj1304  34994  bnj92  35037  bnj124  35046  bnj126  35048  bnj154  35053  bnj155  35054  bnj523  35062  bnj526  35063  bnj540  35067  bnj581  35083  bnj916  35108  bnj929  35111  bnj964  35118  bnj978  35124  bnj983  35126  bnj1039  35146  bnj1040  35147  bnj1123  35161  bnj1128  35165  bnj1398  35209  lfuhgr3  35333  cvmlift2lem1  35515  satfv0  35571  satf0  35585  satf0op  35590  satffunlem  35614  satffunlem1lem1  35615  satffunlem2lem1  35617  elmthm  35789  quad3  35883  3orit  35929  dftr6  35964  eldm3  35974  elrn3  35975  elima4  35989  19.12b  36012  brtxp  36091  brtxp2  36092  brpprod  36096  brpprod3a  36097  elfix  36114  dffix2  36116  ellimits  36121  sscoid  36124  dffun10  36125  elfuns  36126  elsingles  36129  brimg  36148  brapply  36149  lemsuccf  36152  brsuccf  36153  funpartlem  36155  brrestrict  36162  dfrecs2  36163  dfrdg4  36164  brlb  36168  altopthc  36184  altopthd  36185  fvtransport  36245  hfext  36396  ss-ax8  36438  nn0prpw  36536  filnetlem4  36594  df3nandALT2  36613  regsfromregtr  36687  bj-sbeq  37146  bj-csbsnlem  37148  bj-elsngl  37213  bj-eltag  37222  bj-tagex  37232  bj-projun  37239  bj-reabeq  37272  bj-disj2r  37273  bj-axseprep  37319  bj-restuni  37347  bj-elid6  37422  bj-eldiag  37428  bj-eldiag2  37429  topdifinffinlem  37599  relowlpssretop  37616  fvineqsneq  37664  wl-3xorbi  37725  wl-2mintru1  37742  wl-df3maxtru1  37744  wl-dfclab  37837  phpreu  37852  poimirlem24  37892  poimirlem26  37894  poimirlem30  37898  areacirclem5  37960  isbnd2  38031  sbcalf  38362  sbcexf  38363  sbccom2  38373  sbccom2f  38374  sbccom2fi  38375  csbcom2fi  38376  anan  38483  br1cnvinxp  38507  idinxpssinxp2  38572  ineleq  38602  brabidgaw  38621  brabidga  38622  inxpxrn  38666  rnxrn  38669  dfsucmap3  38711  cossssid2  38806  cossssid3  38807  cosscnvssid3  38814  dfeldisj3  39059  dfeldisj4  39060  antisymrelres  39114  dfmembpart2  39121  mpet3  39198  cpet2  39199  prtlem70  39230  prtlem16  39242  ishlat2  39726  pmapglb  40143  polval2N  40279  dicelval3  41553  mapdordlem1a  42007  redvmptabs  42727  fimgmcyclem  42900  fimgmcyc  42901  prjspeclsp  42967  sn-isghm  43028  abbibw  43032  fz1eqin  43123  7rexfrabdioph  43154  rmydioph  43368  dford4  43383  areaquad  43570  onsupmaxb  43593  onov0suclim  43628  nnoeomeqom  43666  tfsconcat0i  43699  faosnf0.11b  43780  ifpan23  43813  ifpdfnan  43839  ifpdfxor  43840  ifpidg  43844  ifpid1g  43847  ifpim123g  43853  ifp1bi  43855  ifpimimb  43857  ifpororb  43858  ifpbibib  43863  rp-fakeuninass  43869  dfsucon  43876  minregex  43887  cllem0  43919  rababg  43927  elmapintrab  43929  elmapintab  43949  undmrnresiss  43957  dfxor4  44119  dfhe3  44128  dffrege115  44331  frege131  44347  frege133  44349  clsk1indlem4  44397  clsk1indlem1  44398  expandrexn  44644  rr-groth  44652  rr-grothshortbi  44656  undisjrab  44659  pm13.196a  44767  eelT11  45059  eelTT1  45062  eelT01  45063  eel0T1  45064  uunTT1  45145  uunTT1p1  45146  uunTT1p2  45147  uunT11  45148  uunT11p1  45149  uunT11p2  45150  uun111  45157  xpwf  45317  permaxinf2lem  45365  permac8prim  45367  ssrabf  45470  rabssf  45475  disjinfi  45548  elicores  45890  fourierdlem42  46504  iundjiun  46815  2reu7  47468  2reu8  47469  2reu8i  47470  dfdfat2  47485  aovov0bi  47553  afv2orxorb  47585  afv2ndeffv0  47617  ichcircshi  47811  ichan  47812  icheq  47819  ichal  47823  prpair  47858  prproropf1olem0  47859  257prm  47918  fmtno4prmfac  47929  nnsum4primeseven  48157  nnsum4primesevenALTV  48158  clnbgrel  48185  isubgr3stgrlem4  48326  usgrexmpl2nb1  48389  usgrexmpl2nb2  48390  gpgprismgr4cycllem10  48461  uspgrsprf1  48504  rrx2xpref1o  49075  iinxp  49187  resinsn  49228  resinsnALT  49229  0funcALT  49444  catcsect  49754  isthincd2  49793  aacllem  50157