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  1530  excxor  1546  cadan  1642  cadcomb  1646  nic-axALT  1707  tbw-bijust  1731  rb-bijust  1782  nf2  1818  19.43  1915  19.43OLD  1916  3exdistr  1993  19.12vvv  2027  sbco4  2139  excom13  2201  sbcom2  2209  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  3656  rexrab2  3658  reu2  3683  rmo4  3688  reu8  3691  rmo3f  3692  2reu5lem3  3715  sbcimdv  3807  reu8nf  3824  rmo2  3834  rmo3  3836  rmoanim  3842  ss2rab  4017  rabss  4018  ssrab  4019  symdifass  4208  dfss4  4215  undi  4231  indifdi  4240  undif3  4246  reuun2  4271  difin0ss  4321  disj  4403  disj4  4412  rabsssn  4629  disjsn  4672  snssb  4743  raldifsni  4758  ssunpr  4794  sspr  4795  sstp  4796  uni0b  4894  uni0c  4895  ssint  4924  intprg  4941  iunssf  5001  iunssfOLD  5002  iunss  5003  iunssOLD  5004  iundif2  5032  disjor  5085  nfnid  5340  reusv2lem4  5366  ssextss  5428  exss  5438  eqvinop  5463  sbcop  5465  opcom  5478  opeqpr  5482  brtp  5501  brabsb  5509  opelopabf  5524  dfid3  5553  pofun  5581  opeliunxp  5722  opeliun2xp  5723  xpiundi  5726  brinxp2  5733  exopxfr  5823  cnvuni  5870  dmopab3  5903  rnep  5911  dmxp  5913  rnopab3  5940  elres  6013  elsnres  6014  elrid  6042  cnvsym  6108  asymref2  6111  intirr  6112  cnvopab  6131  xpeq0  6152  difxp  6156  xpdifid  6160  xpdifcnvepel  6161  ssrnres  6171  dminxp  6173  dfrel4v  6183  elid  6193  dmsnn0  6203  imaco  6247  rnco  6248  rncoOLD  6249  coeq0  6252  resssxp  6267  dfpo2  6294  snres0  6296  sspred  6308  frpoind  6340  sb8iota  6500  fun11  6607  isarep1  6621  dff1o4  6826  opabiota  6960  fvopab5  7020  eqfnfv3  7024  fvn0ssdmfun  7067  fnressn  7155  f13dfv  7275  dff1o6  7276  fliftel  7310  oprabidw  7444  oprabid  7445  eloprabga  7522  mpo2eqb  7545  ralrnmpo  7552  uniuni  7761  dflim3  7843  dfom2  7864  elxp4  7919  elxp5  7920  opabex3d  7962  opabex3rd  7963  opabex3  7964  el2xptp  8032  fsplit  8114  xporderlem  8125  ralxp3f  8135  frpoins3xpg  8138  poxp2  8141  suppvalbr  8162  dfrecs3  8361  tz7.48lem  8430  seqomlem2  8440  oaord  8534  oeeu  8591  nnaord  8607  ecid  8780  mptelixpg  8942  elixpsn  8944  xpsnen  9059  xpcomco  9065  xpassen  9069  omxpenlem  9076  modom  9221  brttrcl2  9693  ttrcltr  9695  rnttrcl  9701  frind  9732  tz9.12lem3  9771  rankxpsuc  9864  cp  9893  cardprclem  9984  infxpenlem  10016  dfac5lem1  10126  dfac5lem2  10127  dfac5lem5  10130  dfac10c  10141  kmlem3  10155  kmlem12  10164  kmlem13  10165  kmlem14  10166  kmlem15  10167  ackbij2  10244  cf0  10252  cflim2  10265  dffin7-2  10400  dfacfin7  10401  fin1a2lem12  10413  axdc3lem3  10454  cfpwsdom  10593  recmulnq  10973  genpass  11018  psslinpr  11040  suplem2pr  11062  opelreal  11139  ltxrlt  11304  addrid  11414  ind1a  12253  elnn0  12530  elxnn0  12603  elnn0z  12628  nnwos  12964  elxr  13167  xrnepnf  13169  elfzuzb  13572  4fvwrd4  13703  preduz  13705  elfzo2  13717  ssnn0fi  14049  sqeqori  14278  xpcogend  15047  cotr2g  15049  fsumcom2  15860  modfsummod  15881  fprodcom2  16071  rpnnen2lem12  16313  gcdcllem1  16589  isprm2  16772  isprm7  16799  pythagtriplem2  16909  infpn2  17005  4sqlem12  17048  initoid  18090  termoid  18091  eldmcoa  18154  oduposb  18415  gsumwspan  18955  smndex1basss  19017  smndex1mgm  19019  isnsg2  19279  isnsg4  19290  cycsubmel  19328  efgcpbllemb  19882  dmdprd  20127  dprdval  20132  dprdw  20139  dprd2d2  20173  dfrhm2  20615  isbrric2  20664  issubrg  20733  isdomn5  20872  islmim  21246  lbsextlem2  21346  prmidl0  21541  cnfldfun  21599  pzriprnglem3  21696  pjfval2  21922  opsrtoslem1  22271  ntreq0  23302  cmpcov2  23615  cmpsub  23625  2ndcdisj  23682  unisngl  23753  txbas  23793  elpt  23798  txkgen  23878  xkococn  23886  fbun  24066  trfil2  24113  fin1aufil  24158  alexsubALTlem3  24275  cnextcn  24293  qustgplem  24347  eltsms  24359  ustn0  24447  fmucndlem  24516  metrest  24750  restmetu  24796  isclmp  25325  srabn  25588  ellogdm  26876  1cubr  27079  leibpilem2  27178  dmarea  27194  vmasum  27452  dchrelbas2  27473  2lgslem4  27642  nosupbnd1lem4  27947  nosupbnd2lem1  27951  lenlts  27988  madeval2  28098  made0  28128  oniso  28536  onsfi  28621  tgcgr4  28873  ltgov  28939  plngrotlem2  29145  axlowdimlem13  29411  axeuclidlem  29419  numedglnl  29601  lfuhgr3  29607  nbupgrres  29824  vtxd0nedgb  29948  rusgrprc  30050  usgr2pth0  30230  wspthsnwspthsnon  30384  isclwwlk  30454  clwwlkn1  30511  clwwlkn2  30514  clwwlknonel  30565  3pthdlem1  30644  iseupthf1o  30682  frgr3v  30755  fusgr2wsp2nb  30814  frgrregord013  30875  h2hcau  31460  h2hlm  31461  shlesb1i  31867  shne0i  31929  chnlei  31966  cmbr2i  32077  pjneli  32204  ho02i  32310  adjsym  32314  adjeu  32370  lnopeqi  32489  largei  32748  atoml2i  32864  cdj3lem3b  32921  or3di  32936  mo5f  32964  dmrab  32972  rabsspr  32976  rabsstp  32977  disjnf  33043  disjorf  33052  ssrelf  33088  ofpreima  33138  disjdsct  33175  1stpreima  33179  2ndpreima  33180  f1od2  33190  xrdifh  33251  nndiffz1  33257  domnprodeq0  33719  zarclsun  34380  ordtconnlem1  34434  measiuns  34728  elunirnmbfm  34763  eulerpartlemr  34885  eulerpartlemgh  34889  eulerpartlemn  34892  ballotlemodife  35009  bnj250  35211  bnj334  35223  bnj345  35224  bnj89  35231  bnj115  35235  bnj919  35277  bnj1304  35328  bnj92  35371  bnj124  35380  bnj126  35382  bnj154  35387  bnj155  35388  bnj523  35396  bnj526  35397  bnj540  35401  bnj581  35417  bnj916  35442  bnj929  35445  bnj964  35452  bnj978  35458  bnj983  35460  bnj1039  35480  bnj1040  35481  bnj1123  35495  bnj1128  35499  bnj1398  35543  cvmlift2lem1  35881  satfv0  35937  satf0  35951  satf0op  35956  satffunlem  35980  satffunlem1lem1  35981  satffunlem2lem1  35983  elmthm  36155  quad3  36249  3orit  36295  dftr6  36330  eldm3  36340  elrn3  36341  elima4  36355  19.12b  36378  brtxp  36457  brtxp2  36458  brpprod  36462  brpprod3a  36463  elfix  36480  dffix2  36482  ellimits  36487  sscoid  36490  dffun10  36491  elfuns  36492  elsingles  36495  brimg  36514  brapply  36515  lemsuccf  36518  brsuccf  36519  funpartlem  36521  brrestrict  36528  dfrecs2  36529  dfrdg4  36530  brlb  36534  dffr7  36535  altopthc  36551  altopthd  36552  fvtransport  36612  hfext  36763  ss-ax8  36845  nn0prpw  36942  filnetlem4  37000  df3nandALT2  37019  regsfromregtco  37157  mh-prprimbi  37162  mh-regprimbi  37164  mh-infprim2bi  37166  mh-infprim3bi  37167  bj-sbeq  37644  bj-csbsnlem  37646  bj-elsngl  37712  bj-eltag  37721  bj-tagex  37731  bj-projun  37738  bj-reabeq  37771  bj-disj2r  37772  bj-axseprep  37819  bj-restuni  37847  bj-elid6  37922  bj-eldiag  37928  bj-eldiag2  37929  topdifinffinlem  38101  relowlpssretop  38118  fvineqsneq  38166  wl-3xorbi  38227  wl-2mintru1  38244  wl-df3maxtru1  38246  wl-dfclab  38348  phpreu  38358  poimirlem24  38393  poimirlem26  38395  poimirlem30  38399  areacirclem5  38461  isbnd2  38533  sbcalf  38862  sbcexf  38863  sbccom2  38873  sbccom2f  38874  sbccom2fi  38875  csbcom2fi  38876  anan  38983  br1cnvinxp  39007  idinxpssinxp2  39072  ineleq  39102  brabidgaw  39121  brabidga  39122  inxpxrn  39166  rnxrn  39169  dfsucmap3  39211  cossssid2  39306  cossssid3  39307  cosscnvssid3  39314  dfeldisj3  39559  dfeldisj4  39560  antisymrelres  39614  dfmembpart2  39621  mpet3  39698  cpet2  39699  prtlem70  39730  prtlem16  39742  ishlat2  40226  pmapglb  40643  polval2N  40779  dicelval3  42053  mapdordlem1a  42507  redvmptabs  43235  fimgmcyclem  43415  fimgmcyc  43416  prjspeclsp  43458  sn-isghm  43519  abbibw  43523  fz1eqin  43614  7rexfrabdioph  43641  rmydioph  43855  dford4  43870  areaquad  44057  onsupmaxb  44080  onov0suclim  44115  nnoeomeqom  44153  tfsconcat0i  44186  faosnf0.11b  44267  ifpan23  44300  ifpdfnan  44326  ifpdfxor  44327  ifpidg  44331  ifpid1g  44334  ifpim123g  44340  ifp1bi  44342  ifpimimb  44344  ifpororb  44345  ifpbibib  44350  rp-fakeuninass  44356  dfsucon  44363  minregex  44374  cllem0  44406  rababg  44414  elmapintrab  44416  elmapintab  44436  undmrnresiss  44444  dfxor4  44606  dfhe3  44615  dffrege115  44818  frege131  44834  frege133  44836  clsk1indlem4  44884  clsk1indlem1  44885  expandrexn  45115  rr-groth  45123  rr-grothshortbi  45127  undisjrab  45130  pm13.196a  45238  eelT11  45529  eelTT1  45532  eelT01  45533  eel0T1  45534  uunTT1  45615  uunTT1p1  45616  uunTT1p2  45617  uunT11  45618  uunT11p1  45619  uunT11p2  45620  uun111  45627  xpwf  45787  permaxinf2lem  45835  permac8prim  45837  ssrabf  45946  rabssf  45951  disjinfi  46024  elicores  46363  fourierdlem42  46977  iundjiun  47288  2reu7  47999  2reu8  48000  2reu8i  48001  dfdfat2  48016  aovov0bi  48084  afv2orxorb  48116  afv2ndeffv0  48148  ichcircshi  48354  ichan  48355  icheq  48362  ichal  48366  prpair  48401  prproropf1olem0  48402  257prm  48464  fmtno4prmfac  48475  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  clnbgrel  48744  isubgr3stgrlem4  48885  usgrexmpl2nb1  48948  usgrexmpl2nb2  48949  gpgprismgr4cycllem10  49020  uspgrsprf1  49063  rrx2xpref1o  49648  iinxp  49759  resinsn  49798  resinsnALT  49799  0funcALT  50014  catcsect  50324  isthincd2  50363  alsanmo  50739  ralsanmo  50740  aacllem  50772