Theorem 3bitri 300

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi1i  341  pm5.32  584  biadan  831  orbi1i  927  orass  935  or32  939  cases  1058  dn1  1073  3anidm  1121  an33rean  1514  nanbi  1529  excxor  1545  cadan  1641  cadcomb  1645  nic-axALT  1706  tbw-bijust  1730  rb-bijust  1781  nf2  1817  19.43  1914  19.43OLD  1915  3exdistr  1992  19.12vvv  2026  sbco4  2138  excom13  2200  sbcom2  2208  sbn  2313  sbnf  2344  19.12vv  2376  eeeanv  2379  ee4anv  2380  ee4anvOLD  2381  2sb8ef  2385  sbel2x  2503  2sb8e  2559  dfmo2  2621  sb8eulem  2623  2mo2  2672  2eu7  2682  2eu8  2683  sbabel  2954  3r19.43  3131  r19.23v  3189  2ralor  3236  rexcom13  3295  cbvreu  3404  rabrabi  3430  cgsex4g  3496  ceqsex2  3500  ceqsex2v  3501  ceqsex3v  3502  ceqsex4v  3503  ceqsex6v  3504  ceqsex8v  3505  ralrab2  3655  rexrab2  3657  reu2  3682  rmo4  3687  reu8  3690  rmo3f  3691  2reu5lem3  3714  sbcimdv  3806  reu8nf  3823  rmo2  3833  rmo3  3835  rmoanim  3841  ss2rab  3994  rabss  3995  ssrab  3996  symdifass  4207  dfss4  4214  undi  4230  indifdi  4239  undif3  4245  reuun2  4270  difin0ss  4320  disj  4402  disj4  4411  rabsssn  4625  disjsn  4668  snssb  4739  raldifsni  4754  ssunpr  4788  sspr  4789  sstp  4790  uni0b  4893  uni0c  4894  ssint  4923  intprg  4940  iunssf  5000  iunssfOLD  5001  iunss  5002  iunssOLD  5003  iundif2  5031  disjor  5084  nfnid  5336  reusv2lem4  5362  ssextss  5420  exss  5430  eqvinop  5455  sbcop  5458  cotsexgw  5462  opcom  5472  opeqpr  5476  brtp  5496  brabsb  5504  opelopabf  5519  dfid3  5548  pofun  5576  opeliunxp  5717  opeliun2xp  5718  xpiundi  5721  brinxp2  5728  el2xptp  5819  exopxfr  5820  cnvuni  5867  dmopab3  5900  rnep  5908  dmxp  5910  rnopab3  5937  elres  6008  elsnres  6009  elrid  6037  cnvsym  6107  asymref2  6110  intirr  6111  cnvopab  6130  xpeq0  6150  difxp  6154  xpdifid  6158  xpdifcnvepel  6159  ssrnres  6169  dminxp  6171  dfrel4v  6181  elid  6193  dmsnn0  6208  imaco  6252  rnco  6253  rncoOLD  6254  coeq0  6257  resssxp  6272  dfpo2  6299  snres0  6301  sspred  6313  frpoind  6345  sb8iota  6505  fun11  6615  isarep1  6629  dff1o4  6834  opabiota  6968  fvopab5  7028  eqfnfv3  7032  fvn0ssdmfun  7075  fnressn  7163  f13dfv  7283  dff1o6  7284  fliftel  7318  oprabidw  7452  oprabid  7453  eloprabga  7530  mpo2eqb  7553  ralrnmpo  7560  uniuni  7777  dflim3  7859  dfom2  7880  elxp4  7935  elxp5  7936  opabex3d  7978  opabex3rd  7979  opabex3  7980  f1od2  8111  fsplit  8131  xporderlem  8142  ralxp3f  8157  frpoins3xpg  8160  poxp2  8163  suppvalbrOLD  8185  dfrecs3  8384  tz7.48lemOLD  8455  seqomlem2  8465  oaord  8559  oeeu  8616  nnaord  8632  ecid  8805  mptelixpg  8967  elixpsn  8969  xpsnen  9084  xpcomco  9090  xpassen  9094  omxpenlem  9101  modom  9246  brttrcl2  9719  ttrcltr  9721  rnttrcl  9727  frind  9758  tz9.12lem3  9800  rankxpsuc  9903  cp  9958  cardprclem  10064  infxpenlem  10096  dfac5lem1  10206  dfac5lem2  10207  dfac5lem5  10210  dfac10c  10221  kmlem3  10235  kmlem12  10244  kmlem13  10245  kmlem14  10246  kmlem15  10247  ackbij2  10324  cf0  10332  cflim2  10345  dffin7-2  10480  dfacfin7  10481  fin1a2lem12  10493  axdc3lem3  10534  cfpwsdom  10673  recmulnq  11053  genpass  11098  psslinpr  11120  suplem2pr  11142  opelreal  11219  ltxrlt  11384  addrid  11494  ind1a  12335  elnn0  12612  elxnn0  12685  elnn0z  12710  nnwos  13046  elxr  13249  xrnepnf  13251  elfzuzb  13654  4fvwrd4  13786  preduz  13788  elfzo2  13800  ssnn0fi  14132  sqeqori  14362  xpcogend  15133  cotr2g  15135  fsumcom2  15946  modfsummod  15967  fprodcom2  16157  rpnnen2lem12  16399  gcdcllem1  16675  isprm2  16863  isprm7  16890  pythagtriplem2  17001  infpn2  17097  4sqlem12  17140  initoid  18182  termoid  18183  eldmcoa  18246  oduposb  18507  gsumwspan  19048  smndex1basss  19110  smndex1mgm  19112  isnsg2  19372  isnsg4  19383  cycsubmel  19421  efgcpbllemb  19975  dmdprd  20220  dprdval  20225  dprdw  20232  dprd2d2  20266  dfrhm2  20710  isbrric2  20759  issubrg  20829  isdomn5  20968  islmim  21343  lbsextlem2  21443  prmidl0  21640  cnfldfun  21698  pzriprnglem3  21795  pjfval2  22021  opsrtoslem1  22370  ntreq0  23401  cmpcov2  23714  cmpsub  23724  2ndcdisj  23781  unisngl  23852  txbas  23892  elpt  23897  txkgen  23977  xkococn  23985  fbun  24165  trfil2  24212  fin1aufil  24257  alexsubALTlem3  24374  cnextcn  24392  qustgplem  24446  eltsms  24458  ustn0  24546  fmucndlem  24615  metrest  24849  restmetu  24895  isclmp  25424  srabn  25687  ellogdm  26973  1cubr  27176  leibpilem2  27275  dmarea  27291  vmasum  27549  dchrelbas2  27570  2lgslem4  27739  nosupbnd1lem4  28074  nosupbnd2lem1  28078  lenlts  28115  madeval2  28225  made0  28255  oniso  28663  onsfi  28748  tgcgr4  29000  ltgov  29066  plngrotlem2  29272  axlowdimlem13  29538  axeuclidlem  29546  numedglnl  29728  lfuhgr3  29734  nbupgrres  29951  vtxd0nedgb  30075  rusgrprc  30177  usgr2pth0  30357  wspthsnwspthsnon  30511  isclwwlk  30581  clwwlkn1  30638  clwwlkn2  30641  clwwlknonel  30692  3pthdlem1  30771  iseupthf1o  30809  frgr3v  30882  fusgr2wsp2nb  30941  frgrregord013  31002  h2hcau  31587  h2hlm  31588  shlesb1i  31994  shne0i  32056  chnlei  32093  cmbr2i  32204  pjneli  32331  ho02i  32437  adjsym  32441  adjeu  32497  lnopeqi  32616  largei  32875  atoml2i  32991  cdj3lem3b  33048  or3di  33105  mo5f  33133  dmrab  33141  rabsspr  33145  rabsstp  33146  disjnf  33212  disjorf  33221  ssrelf  33257  ofpreima  33307  disjdsct  33344  1stpreima  33348  2ndpreima  33349  xrdifh  33419  nndiffz1  33425  domnprodeq0  33887  zarclsun  34549  ordtconnlem1  34603  measiuns  34897  elunirnmbfm  34932  eulerpartlemr  35053  eulerpartlemgh  35057  eulerpartlemn  35060  ballotlemodife  35177  bnj250  35379  bnj334  35391  bnj345  35392  bnj89  35399  bnj115  35403  bnj919  35445  bnj1304  35496  bnj92  35539  bnj124  35548  bnj126  35550  bnj154  35555  bnj155  35556  bnj523  35564  bnj526  35565  bnj540  35569  bnj581  35585  bnj916  35610  bnj929  35613  bnj964  35620  bnj978  35626  bnj983  35628  bnj1039  35648  bnj1040  35649  bnj1123  35663  bnj1128  35667  bnj1398  35711  fwfffunres  35765  rankse  35794  cvmlift2lem1  36154  satfv0  36210  satf0  36224  satf0op  36229  satffunlem  36253  satffunlem1lem1  36254  satffunlem2lem1  36256  elmthm  36428  quad3  36522  3orit  36574  dftr6  36609  eldm3  36619  elrn3  36620  elima4  36633  19.12b  36656  brtxp  36735  brtxp2  36736  brpprod  36740  brpprod3a  36741  elfix  36758  dffix2  36760  ellimits  36765  sscoid  36768  dffun10  36769  elfuns  36770  elsingles  36773  brimg  36792  brapply  36793  lemsuccf  36796  brsuccf  36797  funpartlem  36799  brrestrict  36806  dfrecs2  36807  dfrdg4  36808  brlb  36812  dffr7  36813  altopthc  36829  altopthd  36830  fvtransport  36890  hfext  37027  ss-ax8  37107  nn0prpw  37204  filnetlem4  37262  df3nandALT2  37281  regsfromregtco  37419  mh-prprimbi  37424  mh-regprimbi  37426  mh-infprim2bi  37428  mh-infprim3bi  37429  bj-sbeq  37906  bj-csbsnlem  37908  bj-elsngl  37974  bj-eltag  37983  bj-tagex  37993  bj-projun  38000  bj-reabeq  38033  bj-disj2r  38034  coi1in  38054  bj-axseprep  38083  bj-restuni  38111  bj-elid6  38185  bj-eldiag  38191  bj-eldiag2  38192  topdifinffinlem  38364  relowlpssretop  38381  fvineqsneq  38429  wl-3xorbi  38490  wl-2mintru1  38507  wl-df3maxtru1  38509  wl-dfclab  38611  phpreu  38621  poimirlem24  38656  poimirlem26  38658  poimirlem30  38662  areacirclem5  38724  isbnd2  38811  sbcalf  39140  sbcexf  39141  sbccom2  39151  sbccom2f  39152  sbccom2fi  39153  csbcom2fi  39154  anan  39261  br1cnvinxp  39285  idinxpssinxp2  39350  ineleq  39380  brabidgaw  39399  brabidga  39400  inxpxrn  39444  rnxrn  39447  dfsucmap3  39489  cossssid2  39584  cossssid3  39585  cosscnvssid3  39592  dfeldisj3  39837  dfeldisj4  39838  antisymrelres  39892  dfmembpart2  39899  mpet3  39976  cpet2  39977  prtlem70  40008  prtlem16  40020  ishlat2  40504  pmapglb  40921  polval2N  41057  dicelval3  42331  mapdordlem1a  42785  redvmptabs  43505  fimgmcyclem  43691  fimgmcyc  43692  prjspeclsp  43734  sn-isghm  43778  abbibw  43782  fz1eqin  43874  7rexfrabdioph  43901  rmydioph  44115  dford4  44130  areaquad  44312  onsupmaxb  44335  onov0suclim  44370  nnoeomeqom  44408  tfsconcat0i  44441  faosnf0.11b  44522  ifpan23  44555  ifpdfnan  44581  ifpdfxor  44582  ifpidg  44586  ifpid1g  44589  ifpim123g  44595  ifp1bi  44597  ifpimimb  44599  ifpororb  44600  ifpbibib  44605  rp-fakeuninass  44611  dfsucon  44618  minregex  44629  cllem0  44661  rababg  44669  elmapintrab  44671  elmapintab  44690  undmrnresiss  44698  dfxor4  44860  dfhe3  44869  dffrege115  45072  frege131  45088  frege133  45090  clsk1indlem4  45138  clsk1indlem1  45139  expandrexn  45369  rr-groth  45377  rr-grothshortbi  45381  undisjrab  45384  pm13.196a  45492  eelT11  45783  eelTT1  45786  eelT01  45787  eel0T1  45788  uunTT1  45869  uunTT1p1  45870  uunTT1p2  45871  uunT11  45872  uunT11p1  45873  uunT11p2  45874  uun111  45881  xpwf  46048  permaxinf2lem  46096  permac8prim  46098  ssrabf  46223  rabssf  46228  disjinfi  46301  elicores  46639  fourierdlem42  47253  iundjiun  47564  2reu7  48275  2reu8  48276  2reu8i  48277  dfdfat2  48292  aovov0bi  48360  afv2orxorb  48392  afv2ndeffv0  48424  ichcircshi  48630  ichan  48631  icheq  48638  ichal  48642  prpair  48677  prproropf1olem0  48678  257prm  48740  fmtno4prmfac  48751  nnsum4primeseven  48992  nnsum4primesevenALTV  48993  clnbgrel  49020  isubgr3stgrlem4  49161  usgrexmpl2nb1  49224  usgrexmpl2nb2  49225  gpgprismgr4cycllem10  49296  uspgrsprf1  49339  iinxp  50036  resinsn  50079  resinsnALT  50080  0funcALT  50297  catcsect  50627  isthincd2  50666  alsanmo  51075  ralsanmo  51076  aacllem  51108