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  1515  nanbi  1530  excxor  1546  cadan  1642  cadcomb  1646  nic-axALT  1707  tbw-bijust  1731  rb-bijust  1782  nf2  1818  19.43  1917  19.43OLD  1918  3exdistr  1995  19.12vvv  2029  sbco4  2141  excom13  2204  sbcom2  2212  sbn  2317  sbnf  2348  19.12vv  2380  eeeanv  2383  ee4anv  2384  2sb8ef  2388  sbel2x  2506  2sb8e  2562  dfmo2  2624  sb8eulem  2626  2mo2  2675  2eu7  2685  2eu8  2686  sbabel  2958  3r19.43  3135  r19.23v  3193  2ralor  3240  rexcom13  3299  cbvreu  3408  rabrabi  3434  cgsex4g  3500  ceqsex2  3504  ceqsex2v  3505  ceqsex3v  3506  ceqsex4v  3507  ceqsex6v  3508  ceqsex8v  3509  ralrab2  3659  rexrab2  3661  reu2  3686  rmo4  3691  reu8  3694  rmo3f  3695  2reu5lem3  3718  sbcimdv  3810  reu8nf  3828  rmo2  3838  rmo3  3840  rmoanim  3846  ss2rab  3997  rabss  3998  ssrab  3999  symdifass  4210  dfss4  4217  undi  4233  indifdi  4242  undif3  4248  reuun2  4273  noel  4286  difin0ss  4324  disj  4406  disj4  4415  rabsssn  4629  disjsn  4672  snssb  4743  raldifsni  4758  ssunpr  4792  sspr  4793  sstp  4794  uni0b  4897  uni0c  4898  ssint  4927  intprg  4944  iunssf  5004  iunssfOLD  5005  iunss  5006  iunssOLD  5007  iundif2  5035  disjor  5088  nfnid  5342  reusv2lem4  5368  ssextss  5426  exss  5436  eqvinop  5461  sbcop  5464  cotsexgw  5468  opcom  5478  opeqpr  5482  brtp  5502  brabsb  5510  opelopabf  5525  dfid3  5554  pofun  5582  opeliunxp  5723  opeliun2xp  5724  xpiundi  5727  elvv  5731  brinxp2  5735  el2xptp  5828  exopxfr  5829  cnvuni  5878  dmopab3  5911  rnep  5919  dmxp  5921  rnopab3  5948  elres  6025  elsnres  6026  elrid  6054  cnvsym  6124  asymref2  6127  intirr  6128  cnvopab  6147  xpeq0  6167  difxp  6171  xpdifid  6175  xpdifcnvepel  6176  ssrnres  6186  dminxp  6188  dfrel4v  6198  elid  6210  dmsnn0  6225  imaco  6269  rnco  6270  rncoOLD  6271  coeq0  6274  resssxp  6294  dfpo2  6323  snres0  6325  sspred  6337  frpoind  6369  sb8iota  6529  fun11  6642  isarep1  6656  dff1o4  6861  opabiota  6996  fvopab5  7056  eqfnfv3  7060  fvn0ssdmfun  7104  fnressn  7192  f13dfv  7311  dff1o6  7312  fliftel  7346  oprabidw  7480  oprabid  7481  eloprabga  7558  mpo2eqb  7581  ralrnmpo  7589  uniuni  7806  dflim3  7890  dfom2  7911  elxp4  7966  elxp5  7967  opabex3d  8009  opabex3rd  8010  opabex3  8011  f1od2  8143  fsplit  8163  xporderlem  8174  ralxp3f  8189  frpoins3xpg  8192  poxp2  8195  suppvalbrOLD  8217  dfrecs3  8416  tz7.48lemOLD  8487  seqomlem2  8497  oaord  8591  oeeu  8648  nnaord  8664  ecid  8837  mptelixpg  8999  elixpsn  9001  xpsnen  9116  xpcomco  9122  xpassen  9126  omxpenlem  9133  modom  9278  brttrcl2  9750  ttrcltr  9752  rnttrcl  9758  frind  9789  tz9.12lem3  9831  rankxpsuc  9934  cp  9989  cardprclem  10095  infxpenlem  10129  dfac5lem1  10239  dfac5lem2  10240  dfac5lem5  10243  dfac10c  10254  kmlem3  10268  kmlem12  10277  kmlem13  10278  kmlem14  10279  kmlem15  10280  ackbij2  10357  cf0  10365  cflim2  10378  dffin7-2  10513  dfacfin7  10514  fin1a2lem12  10526  axdc3lem3  10567  cfpwsdom  10706  recmulnq  11086  genpass  11131  psslinpr  11153  suplem2pr  11175  opelreal  11252  ltxrlt  11417  addrid  11527  ind1a  12369  elnn0  12646  elxnn0  12719  elnn0z  12744  nnwos  13080  elxr  13283  xrnepnf  13285  elfzuzb  13688  4fvwrd4  13820  preduz  13822  elfzo2  13834  ssnn0fi  14166  sqeqori  14397  xpcogend  15168  cotr2g  15170  fsumcom2  15981  modfsummod  16002  fprodcom2  16192  rpnnen2lem12  16434  gcdcllem1  16710  isprm2  16898  isprm7  16925  pythagtriplem2  17036  infpn2  17132  4sqlem12  17175  initoid  18217  termoid  18218  eldmcoa  18281  oduposb  18542  gsumwspan  19083  smndex1basss  19145  smndex1mgm  19147  isnsg2  19407  isnsg4  19418  cycsubmel  19456  efgcpbllemb  20011  dmdprd  20256  dprdval  20261  dprdw  20268  dprd2d2  20302  dfrhm2  20746  isbrric2  20795  issubrg  20865  isdomn5  21004  islmim  21379  lbsextlem2  21479  prmidl0  21676  cnfldfun  21734  pzriprnglem3  21833  pjfval2  22059  opsrtoslem1  22408  ntreq0  23439  cmpcov2  23752  cmpsub  23762  2ndcdisj  23819  unisngl  23890  txbas  23930  elpt  23935  txkgen  24015  xkococn  24023  fbun  24203  trfil2  24250  fin1aufil  24295  alexsubALTlem3  24412  cnextcn  24430  qustgplem  24484  eltsms  24496  ustn0  24584  fmucndlem  24653  metrest  24887  restmetu  24933  isclmp  25462  srabn  25725  ellogdm  27013  1cubr  27216  leibpilem2  27315  dmarea  27331  vmasum  27589  dchrelbas2  27610  2lgslem4  27779  nosupbnd1lem4  28114  nosupbnd2lem1  28118  lenlts  28155  madeval2  28265  made0  28295  oniso  28703  onsfi  28788  tgcgr4  29040  ltgov  29106  plngrotlem2  29312  axlowdimlem13  29578  axeuclidlem  29586  numedglnl  29768  lfuhgr3  29774  nbupgrres  29991  vtxd0nedgb  30115  rusgrprc  30217  usgr2pth0  30397  wspthsnwspthsnon  30551  isclwwlk  30621  clwwlkn1  30678  clwwlkn2  30681  clwwlknonel  30732  3pthdlem1  30811  iseupthf1o  30849  frgr3v  30922  fusgr2wsp2nb  30981  frgrregord013  31042  h2hcau  31627  h2hlm  31628  shlesb1i  32034  shne0i  32096  chnlei  32133  cmbr2i  32244  pjneli  32371  ho02i  32477  adjsym  32481  adjeu  32537  lnopeqi  32656  largei  32915  atoml2i  33031  cdj3lem3b  33088  or3di  33145  mo5f  33173  dmrab  33181  rabsspr  33185  rabsstp  33186  disjnf  33252  disjorf  33261  ssrelf  33297  ofpreima  33347  disjdsct  33383  1stpreima  33387  2ndpreima  33388  xrdifh  33458  nndiffz1  33464  domnprodeq0  33929  zarclsun  34606  ordtconnlem1  34660  measiuns  34954  elunirnmbfm  34989  eulerpartlemr  35110  eulerpartlemgh  35114  eulerpartlemn  35117  ballotlemodife  35234  bnj250  35436  bnj334  35448  bnj345  35449  bnj89  35456  bnj115  35460  bnj919  35502  bnj1304  35553  bnj92  35596  bnj124  35605  bnj126  35607  bnj154  35612  bnj155  35613  bnj523  35621  bnj526  35622  bnj540  35626  bnj581  35642  bnj916  35667  bnj929  35670  bnj964  35677  bnj978  35683  bnj983  35685  bnj1039  35705  bnj1040  35706  bnj1123  35720  bnj1128  35724  bnj1398  35768  fwfffunres  35822  rankse  35857  cvmlift2lem1  36268  satfv0  36324  satf0  36338  satf0op  36343  satffunlem  36367  satffunlem1lem1  36368  satffunlem2lem1  36370  elmthm  36542  quad3  36636  3orit  36689  dftr6  36724  eldm3  36734  elrn3  36735  elima4  36748  19.12b  36771  brtxp  36850  brtxp2  36851  brpprod  36855  brpprod3a  36856  elfix  36873  dffix2  36875  ellimits  36880  sscoid  36883  dffun10  36884  elfuns  36885  elsingles  36888  brimg  36907  brapply  36908  lemsuccf  36911  brsuccf  36912  funpartlem  36914  brrestrict  36921  dfrecs2  36922  dfrdg4  36923  brlb  36927  dffr7  36928  altopthc  36944  altopthd  36945  fvtransport  37005  hfext  37142  ss-ax8  37222  nn0prpw  37319  filnetlem4  37377  df3nandALT2  37396  regsfromregtco  37534  mh-prprimbi  37539  mh-regprimbi  37541  mh-infprim2bi  37543  mh-infprim3bi  37544  bj-sbeq  38021  bj-csbsnlem  38023  bj-elsngl  38089  bj-eltag  38098  bj-tagex  38108  bj-projun  38115  bj-reabeq  38148  bj-disj2r  38149  bj-elinxp  38170  bj-elres  38177  bj-axseprep  38253  bj-restuni  38281  bj-elid6  38352  bj-eldiag  38358  bj-eldiag2  38359  topdifinffinlem  38531  relowlpssretop  38548  fvineqsneq  38596  wl-3xorbi  38657  wl-2mintru1  38674  wl-df3maxtru1  38676  wl-dfclab  38778  phpreu  38788  poimirlem24  38823  poimirlem26  38825  poimirlem30  38829  areacirclem5  38891  isbnd2  38976  sbcalf  39305  sbcexf  39306  sbccom2  39316  sbccom2f  39317  sbccom2fi  39318  csbcom2fi  39319  anan  39426  br1cnvinxp  39450  idinxpssinxp2  39515  ineleq  39545  brabidgaw  39564  brabidga  39565  inxpxrn  39609  rnxrn  39612  dfsucmap3  39654  cossssid2  39749  cossssid3  39750  cosscnvssid3  39757  dfeldisj3  40002  dfeldisj4  40003  antisymrelres  40057  dfmembpart2  40064  mpet3  40141  cpet2  40142  prtlem70  40173  prtlem16  40185  ishlat2  40669  pmapglb  41086  polval2N  41222  dicelval3  42496  mapdordlem1a  42950  redvmptabs  43671  fimgmcyclem  43857  fimgmcyc  43858  prjspeclsp  43900  sn-isghm  43944  abbibw  43948  fz1eqin  44040  7rexfrabdioph  44067  rmydioph  44281  dford4  44296  areaquad  44473  onsupmaxb  44496  onov0suclim  44531  nnoeomeqom  44569  tfsconcat0i  44602  faosnf0.11b  44683  ifpan23  44716  ifpdfnan  44742  ifpdfxor  44743  ifpidg  44747  ifpid1g  44750  ifpim123g  44756  ifp1bi  44758  ifpimimb  44760  ifpororb  44761  ifpbibib  44766  rp-fakeuninass  44772  dfsucon  44779  minregex  44790  cllem0  44822  rababg  44830  elmapintrab  44832  elmapintab  44851  undmrnresiss  44859  dfxor4  45021  dfhe3  45030  dffrege115  45233  frege131  45249  frege133  45251  clsk1indlem4  45299  clsk1indlem1  45300  expandrexn  45530  rr-groth  45538  rr-grothshortbi  45542  undisjrab  45545  pm13.196a  45653  eelT11  45943  eelTT1  45946  eelT01  45947  eel0T1  45948  uunTT1  46029  uunTT1p1  46030  uunTT1p2  46031  uunT11  46032  uunT11p1  46033  uunT11p2  46034  uun111  46041  xpwf  46212  permaxinf2lem  46260  permac8prim  46262  ssrabf  46396  rabssf  46401  disjinfi  46474  elicores  46812  fourierdlem42  47426  iundjiun  47737  2reu7  48449  2reu8  48450  2reu8i  48451  dfdfat2  48465  aovov0bi  48533  afv2orxorb  48565  afv2ndeffv0  48597  ichcircshi  48803  ichan  48804  icheq  48811  ichal  48815  prpair  48850  prproropf1olem0  48851  257prm  48913  fmtno4prmfac  48924  nnsum4primeseven  49165  nnsum4primesevenALTV  49166  clnbgrel  49193  isubgr3stgrlem4  49334  usgrexmpl2nb1  49397  usgrexmpl2nb2  49398  gpgprismgr4cycllem10  49469  uspgrsprf1  49512  iinxp  50267  resinsn  50310  resinsnALT  50311  0funcALT  50528  catcsect  50858  isthincd2  50897  alsanmo  51328  ralsanmo  51329  aacllem  51361