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  2314  sbnf  2345  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  3132  r19.23v  3190  2ralor  3237  rexcom13  3296  cbvreu  3405  rabrabi  3431  cgsex4g  3497  ceqsex2  3501  ceqsex2v  3502  ceqsex3v  3503  ceqsex4v  3504  ceqsex6v  3505  ceqsex8v  3506  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  5337  reusv2lem4  5363  ssextss  5421  exss  5431  eqvinop  5456  sbcop  5459  cotsexgw  5463  opcom  5473  opeqpr  5477  brtp  5497  brabsb  5505  opelopabf  5520  dfid3  5549  pofun  5577  opeliunxp  5718  opeliun2xp  5719  xpiundi  5722  brinxp2  5729  el2xptp  5820  exopxfr  5821  cnvuni  5868  dmopab3  5901  rnep  5909  dmxp  5911  rnopab3  5938  elres  6009  elsnres  6010  elrid  6038  cnvsym  6108  asymref2  6111  intirr  6112  cnvopab  6131  xpeq0  6151  difxp  6155  xpdifid  6159  xpdifcnvepel  6160  ssrnres  6170  dminxp  6172  dfrel4v  6182  elid  6192  dmsnn0  6207  imaco  6251  rnco  6252  rncoOLD  6253  coeq0  6256  resssxp  6271  dfpo2  6298  snres0  6300  sspred  6312  frpoind  6344  sb8iota  6504  fun11  6612  isarep1  6626  dff1o4  6831  opabiota  6965  fvopab5  7025  eqfnfv3  7029  fvn0ssdmfun  7072  fnressn  7160  f13dfv  7280  dff1o6  7281  fliftel  7315  oprabidw  7449  oprabid  7450  eloprabga  7527  mpo2eqb  7550  ralrnmpo  7557  uniuni  7774  dflim3  7856  dfom2  7877  elxp4  7932  elxp5  7933  opabex3d  7975  opabex3rd  7976  opabex3  7977  fsplit  8126  xporderlem  8137  ralxp3f  8147  frpoins3xpg  8150  poxp2  8153  suppvalbr  8174  dfrecs3  8373  tz7.48lemOLD  8444  seqomlem2  8454  oaord  8548  oeeu  8605  nnaord  8621  ecid  8794  mptelixpg  8956  elixpsn  8958  xpsnen  9073  xpcomco  9079  xpassen  9083  omxpenlem  9090  modom  9235  brttrcl2  9708  ttrcltr  9710  rnttrcl  9716  frind  9747  tz9.12lem3  9789  rankxpsuc  9892  cp  9947  cardprclem  10053  infxpenlem  10085  dfac5lem1  10195  dfac5lem2  10196  dfac5lem5  10199  dfac10c  10210  kmlem3  10224  kmlem12  10233  kmlem13  10234  kmlem14  10235  kmlem15  10236  ackbij2  10313  cf0  10321  cflim2  10334  dffin7-2  10469  dfacfin7  10470  fin1a2lem12  10482  axdc3lem3  10523  cfpwsdom  10662  recmulnq  11042  genpass  11087  psslinpr  11109  suplem2pr  11131  opelreal  11208  ltxrlt  11373  addrid  11483  ind1a  12324  elnn0  12601  elxnn0  12674  elnn0z  12699  nnwos  13035  elxr  13238  xrnepnf  13240  elfzuzb  13643  4fvwrd4  13775  preduz  13777  elfzo2  13789  ssnn0fi  14121  sqeqori  14351  xpcogend  15120  cotr2g  15122  fsumcom2  15933  modfsummod  15954  fprodcom2  16144  rpnnen2lem12  16386  gcdcllem1  16662  isprm2  16850  isprm7  16877  pythagtriplem2  16988  infpn2  17084  4sqlem12  17127  initoid  18169  termoid  18170  eldmcoa  18233  oduposb  18494  gsumwspan  19035  smndex1basss  19097  smndex1mgm  19099  isnsg2  19359  isnsg4  19370  cycsubmel  19408  efgcpbllemb  19962  dmdprd  20207  dprdval  20212  dprdw  20219  dprd2d2  20253  dfrhm2  20697  isbrric2  20746  issubrg  20816  isdomn5  20955  islmim  21330  lbsextlem2  21430  prmidl0  21627  cnfldfun  21685  pzriprnglem3  21782  pjfval2  22008  opsrtoslem1  22357  ntreq0  23388  cmpcov2  23701  cmpsub  23711  2ndcdisj  23768  unisngl  23839  txbas  23879  elpt  23884  txkgen  23964  xkococn  23972  fbun  24152  trfil2  24199  fin1aufil  24244  alexsubALTlem3  24361  cnextcn  24379  qustgplem  24433  eltsms  24445  ustn0  24533  fmucndlem  24602  metrest  24836  restmetu  24882  isclmp  25411  srabn  25674  ellogdm  26960  1cubr  27163  leibpilem2  27262  dmarea  27278  vmasum  27536  dchrelbas2  27557  2lgslem4  27726  nosupbnd1lem4  28061  nosupbnd2lem1  28065  lenlts  28102  madeval2  28212  made0  28242  oniso  28650  onsfi  28735  tgcgr4  28987  ltgov  29053  plngrotlem2  29259  axlowdimlem13  29525  axeuclidlem  29533  numedglnl  29715  lfuhgr3  29721  nbupgrres  29938  vtxd0nedgb  30062  rusgrprc  30164  usgr2pth0  30344  wspthsnwspthsnon  30498  isclwwlk  30568  clwwlkn1  30625  clwwlkn2  30628  clwwlknonel  30679  3pthdlem1  30758  iseupthf1o  30796  frgr3v  30869  fusgr2wsp2nb  30928  frgrregord013  30989  h2hcau  31574  h2hlm  31575  shlesb1i  31981  shne0i  32043  chnlei  32080  cmbr2i  32191  pjneli  32318  ho02i  32424  adjsym  32428  adjeu  32484  lnopeqi  32603  largei  32862  atoml2i  32978  cdj3lem3b  33035  or3di  33050  mo5f  33078  dmrab  33086  rabsspr  33090  rabsstp  33091  disjnf  33157  disjorf  33166  ssrelf  33202  ofpreima  33252  disjdsct  33289  1stpreima  33293  2ndpreima  33294  f1od2  33304  xrdifh  33365  nndiffz1  33371  domnprodeq0  33833  zarclsun  34495  ordtconnlem1  34549  measiuns  34843  elunirnmbfm  34878  eulerpartlemr  34999  eulerpartlemgh  35003  eulerpartlemn  35006  ballotlemodife  35123  bnj250  35325  bnj334  35337  bnj345  35338  bnj89  35345  bnj115  35349  bnj919  35391  bnj1304  35442  bnj92  35485  bnj124  35494  bnj126  35496  bnj154  35501  bnj155  35502  bnj523  35510  bnj526  35511  bnj540  35515  bnj581  35531  bnj916  35556  bnj929  35559  bnj964  35566  bnj978  35572  bnj983  35574  bnj1039  35594  bnj1040  35595  bnj1123  35609  bnj1128  35613  bnj1398  35657  cvmlift2lem1  36046  satfv0  36102  satf0  36116  satf0op  36121  satffunlem  36145  satffunlem1lem1  36146  satffunlem2lem1  36148  elmthm  36320  quad3  36414  3orit  36460  dftr6  36495  eldm3  36505  elrn3  36506  elima4  36520  19.12b  36543  brtxp  36622  brtxp2  36623  brpprod  36627  brpprod3a  36628  elfix  36645  dffix2  36647  ellimits  36652  sscoid  36655  dffun10  36656  elfuns  36657  elsingles  36660  brimg  36679  brapply  36680  lemsuccf  36683  brsuccf  36684  funpartlem  36686  brrestrict  36693  dfrecs2  36694  dfrdg4  36695  brlb  36699  dffr7  36700  altopthc  36716  altopthd  36717  fvtransport  36777  hfext  36914  ss-ax8  36994  nn0prpw  37091  filnetlem4  37149  df3nandALT2  37168  regsfromregtco  37306  mh-prprimbi  37311  mh-regprimbi  37313  mh-infprim2bi  37315  mh-infprim3bi  37316  bj-sbeq  37793  bj-csbsnlem  37795  bj-elsngl  37861  bj-eltag  37870  bj-tagex  37880  bj-projun  37887  bj-reabeq  37920  bj-disj2r  37921  coi1in  37941  bj-axseprep  37970  bj-restuni  37998  bj-elid6  38071  bj-eldiag  38077  bj-eldiag2  38078  topdifinffinlem  38250  relowlpssretop  38267  fvineqsneq  38315  wl-3xorbi  38376  wl-2mintru1  38393  wl-df3maxtru1  38395  wl-dfclab  38497  phpreu  38507  poimirlem24  38542  poimirlem26  38544  poimirlem30  38548  areacirclem5  38610  isbnd2  38697  sbcalf  39026  sbcexf  39027  sbccom2  39037  sbccom2f  39038  sbccom2fi  39039  csbcom2fi  39040  anan  39147  br1cnvinxp  39171  idinxpssinxp2  39236  ineleq  39266  brabidgaw  39285  brabidga  39286  inxpxrn  39330  rnxrn  39333  dfsucmap3  39375  cossssid2  39470  cossssid3  39471  cosscnvssid3  39478  dfeldisj3  39723  dfeldisj4  39724  antisymrelres  39778  dfmembpart2  39785  mpet3  39862  cpet2  39863  prtlem70  39894  prtlem16  39906  ishlat2  40390  pmapglb  40807  polval2N  40943  dicelval3  42217  mapdordlem1a  42671  redvmptabs  43391  fimgmcyclem  43577  fimgmcyc  43578  prjspeclsp  43620  sn-isghm  43664  abbibw  43668  fz1eqin  43759  7rexfrabdioph  43786  rmydioph  44000  dford4  44015  areaquad  44202  onsupmaxb  44225  onov0suclim  44260  nnoeomeqom  44298  tfsconcat0i  44331  faosnf0.11b  44412  ifpan23  44445  ifpdfnan  44471  ifpdfxor  44472  ifpidg  44476  ifpid1g  44479  ifpim123g  44485  ifp1bi  44487  ifpimimb  44489  ifpororb  44490  ifpbibib  44495  rp-fakeuninass  44501  dfsucon  44508  minregex  44519  cllem0  44551  rababg  44559  elmapintrab  44561  elmapintab  44581  undmrnresiss  44589  dfxor4  44751  dfhe3  44760  dffrege115  44963  frege131  44979  frege133  44981  clsk1indlem4  45029  clsk1indlem1  45030  expandrexn  45260  rr-groth  45268  rr-grothshortbi  45272  undisjrab  45275  pm13.196a  45383  eelT11  45674  eelTT1  45677  eelT01  45678  eel0T1  45679  uunTT1  45760  uunTT1p1  45761  uunTT1p2  45762  uunT11  45763  uunT11p1  45764  uunT11p2  45765  uun111  45772  xpwf  45932  permaxinf2lem  45980  permac8prim  45982  ssrabf  46098  rabssf  46103  disjinfi  46176  elicores  46514  fourierdlem42  47128  iundjiun  47439  2reu7  48150  2reu8  48151  2reu8i  48152  dfdfat2  48167  aovov0bi  48235  afv2orxorb  48267  afv2ndeffv0  48299  ichcircshi  48505  ichan  48506  icheq  48513  ichal  48517  prpair  48552  prproropf1olem0  48553  257prm  48615  fmtno4prmfac  48626  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  clnbgrel  48895  isubgr3stgrlem4  49036  usgrexmpl2nb1  49099  usgrexmpl2nb2  49100  gpgprismgr4cycllem10  49171  uspgrsprf1  49214  rrx2xpref1o  49799  iinxp  49910  resinsn  49949  resinsnALT  49950  0funcALT  50165  catcsect  50475  isthincd2  50514  alsanmo  50875  ralsanmo  50876  aacllem  50908