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  3382  rabrabi  3409  cgsex4g  3477  ceqsex2  3482  ceqsex2v  3483  ceqsex3v  3484  ceqsex4v  3485  ceqsex6v  3486  ceqsex8v  3487  ralrab2  3645  rexrab2  3647  reu2  3672  rmo4  3677  reu8  3680  rmo3f  3681  2reu5lem3  3704  sbcimdv  3798  reu8nf  3816  rmo2  3826  rmo3  3828  rmoanim  3833  ss2rab  4010  rabss  4011  ssrab  4012  dfdif3OLD  4059  symdifass  4203  dfss4  4210  undi  4226  indifdi  4235  undif3  4241  reuun2  4266  difin0ss  4314  disj  4391  disj4  4400  rabsssn  4613  disjsn  4656  snssb  4727  raldifsni  4739  ssunpr  4778  sspr  4779  sstp  4780  uni0b  4877  uni0c  4878  ssint  4907  intprg  4924  iunssf  4986  iunssfOLD  4987  iunss  4988  iunssOLD  4989  iundif2  5017  disjor  5068  nfnid  5312  reusv2lem4  5338  ssextss  5400  exss  5410  eqvinop  5435  sbcop  5437  opcom  5449  opeqpr  5453  brtp  5471  brabsb  5479  opelopabf  5493  dfid3  5522  pofun  5550  opeliunxp  5691  opeliun2xp  5692  xpiundi  5695  brinxp2  5702  exopxfr  5792  cnvuni  5835  dmopab3  5868  rnep  5876  dmxp  5878  rnopab3  5905  elres  5979  elsnres  5980  elrid  6005  cnvsym  6071  asymref2  6074  intirr  6075  cnvopab  6094  xpeq0  6118  difxp  6122  xpdifid  6126  ssrnres  6136  dminxp  6138  dfrel4v  6148  elid  6157  dmsnn0  6165  imaco  6209  rnco  6210  rncoOLD  6211  coeq0  6214  resssxp  6228  dfpo2  6254  snres0  6256  sspred  6268  frpoind  6300  sb8iota  6459  fun11  6566  isarep1  6581  dff1o4  6782  opabiota  6916  fvopab5  6975  eqfnfv3  6979  fvn0ssdmfun  7020  fnressn  7105  f13dfv  7222  dff1o6  7223  fliftel  7257  oprabidw  7391  oprabid  7392  eloprabga  7469  mpo2eqb  7492  ralrnmpo  7499  uniuni  7709  dflim3  7791  dfom2  7812  elxp4  7866  elxp5  7867  opabex3d  7911  opabex3rd  7912  opabex3  7913  el2xptp  7981  fsplit  8060  xporderlem  8070  ralxp3f  8080  frpoins3xpg  8083  poxp2  8086  suppvalbr  8107  dfrecs3  8305  tz7.48lem  8373  seqomlem2  8383  oaord  8475  oeeu  8532  nnaord  8548  ecid  8720  mptelixpg  8876  elixpsn  8878  xpsnen  8992  xpcomco  8998  xpassen  9002  omxpenlem  9009  modom  9154  brttrcl2  9626  ttrcltr  9628  rnttrcl  9634  frind  9665  tz9.12lem3  9704  rankxpsuc  9797  cp  9806  cardprclem  9894  infxpenlem  9926  dfac5lem1  10036  dfac5lem2  10037  dfac5lem5  10040  dfac10c  10052  kmlem3  10066  kmlem12  10075  kmlem13  10076  kmlem14  10077  kmlem15  10078  ackbij2  10155  cf0  10164  cflim2  10176  dffin7-2  10311  dfacfin7  10312  fin1a2lem12  10324  axdc3lem3  10365  cfpwsdom  10498  recmulnq  10878  genpass  10923  psslinpr  10945  suplem2pr  10967  opelreal  11044  ltxrlt  11207  addrid  11317  ind1a  12161  elnn0  12430  elxnn0  12503  elnn0z  12528  nnwos  12856  elxr  13058  xrnepnf  13060  elfzuzb  13463  4fvwrd4  13593  preduz  13595  elfzo2  13607  ssnn0fi  13938  sqeqori  14167  xpcogend  14927  cotr2g  14929  fsumcom2  15727  modfsummod  15748  fprodcom2  15940  rpnnen2lem12  16183  gcdcllem1  16459  isprm2  16642  isprm7  16669  pythagtriplem2  16779  infpn2  16875  4sqlem12  16918  initoid  17959  termoid  17960  eldmcoa  18023  oduposb  18284  gsumwspan  18805  smndex1basss  18867  smndex1mgm  18869  isnsg2  19122  isnsg4  19133  cycsubmel  19166  efgcpbllemb  19721  dmdprd  19966  dprdval  19971  dprdw  19978  dprd2d2  20012  dfrhm2  20445  brric2  20474  issubrg  20539  isdomn5  20678  islmim  21049  lbsextlem2  21149  cnfldfun  21358  cnfldfunOLD  21371  pzriprnglem3  21473  pjfval2  21699  opsrtoslem1  22043  ntreq0  23052  cmpcov2  23365  cmpsub  23375  2ndcdisj  23431  unisngl  23502  txbas  23542  elpt  23547  txkgen  23627  xkococn  23635  fbun  23815  trfil2  23862  fin1aufil  23907  alexsubALTlem3  24024  cnextcn  24042  qustgplem  24096  eltsms  24108  ustn0  24196  fmucndlem  24265  metrest  24499  restmetu  24545  isclmp  25074  srabn  25337  ellogdm  26616  1cubr  26819  leibpilem2  26918  dmarea  26934  vmasum  27193  dchrelbas2  27214  2lgslem4  27383  nosupbnd1lem4  27689  nosupbnd2lem1  27693  lenlts  27730  madeval2  27839  made0  27869  oniso  28277  onsfi  28362  tgcgr4  28613  ltgov  28679  axlowdimlem13  29037  axeuclidlem  29045  numedglnl  29227  nbupgrres  29447  vtxd0nedgb  29572  rusgrprc  29674  usgr2pth0  29848  wspthsnwspthsnon  29999  isclwwlk  30069  clwwlkn1  30126  clwwlkn2  30129  clwwlknonel  30180  3pthdlem1  30249  iseupthf1o  30287  frgr3v  30360  fusgr2wsp2nb  30419  frgrregord013  30480  h2hcau  31065  h2hlm  31066  shlesb1i  31472  shne0i  31534  chnlei  31571  cmbr2i  31682  pjneli  31809  ho02i  31915  adjsym  31919  adjeu  31975  lnopeqi  32094  largei  32353  atoml2i  32469  cdj3lem3b  32526  or3di  32543  mo5f  32573  dmrab  32581  rabsspr  32586  rabsstp  32587  disjnf  32655  disjorf  32664  ssrelf  32703  ofpreima  32753  disjdsct  32791  1stpreima  32795  2ndpreima  32796  f1od2  32807  xrdifh  32868  nndiffz1  32874  domnprodeq0  33352  prmidl0  33525  zarclsun  34030  ordtconnlem1  34084  measiuns  34377  elunirnmbfm  34412  eulerpartlemr  34534  eulerpartlemgh  34538  eulerpartlemn  34541  ballotlemodife  34658  bnj250  34860  bnj334  34872  bnj345  34873  bnj89  34880  bnj115  34884  bnj919  34926  bnj1304  34977  bnj92  35020  bnj124  35029  bnj126  35031  bnj154  35036  bnj155  35037  bnj523  35045  bnj526  35046  bnj540  35050  bnj581  35066  bnj916  35091  bnj929  35094  bnj964  35101  bnj978  35107  bnj983  35109  bnj1039  35129  bnj1040  35130  bnj1123  35144  bnj1128  35148  bnj1398  35192  lfuhgr3  35318  cvmlift2lem1  35500  satfv0  35556  satf0  35570  satf0op  35575  satffunlem  35599  satffunlem1lem1  35600  satffunlem2lem1  35602  elmthm  35774  quad3  35868  3orit  35914  dftr6  35949  eldm3  35959  elrn3  35960  elima4  35974  19.12b  35997  brtxp  36076  brtxp2  36077  brpprod  36081  brpprod3a  36082  elfix  36099  dffix2  36101  ellimits  36106  sscoid  36109  dffun10  36110  elfuns  36111  elsingles  36114  brimg  36133  brapply  36134  lemsuccf  36137  brsuccf  36138  funpartlem  36140  brrestrict  36147  dfrecs2  36148  dfrdg4  36149  brlb  36153  altopthc  36169  altopthd  36170  fvtransport  36230  hfext  36381  ss-ax8  36423  nn0prpw  36521  filnetlem4  36579  df3nandALT2  36598  regsfromregtco  36736  mh-prprimbi  36741  mh-regprimbi  36743  mh-infprim2bi  36745  mh-infprim3bi  36746  bj-sbeq  37224  bj-csbsnlem  37226  bj-elsngl  37291  bj-eltag  37300  bj-tagex  37310  bj-projun  37317  bj-reabeq  37350  bj-disj2r  37351  bj-axseprep  37397  bj-restuni  37425  bj-elid6  37500  bj-eldiag  37506  bj-eldiag2  37507  topdifinffinlem  37677  relowlpssretop  37694  fvineqsneq  37742  wl-3xorbi  37803  wl-2mintru1  37820  wl-df3maxtru1  37822  wl-dfclab  37924  phpreu  37939  poimirlem24  37979  poimirlem26  37981  poimirlem30  37985  areacirclem5  38047  isbnd2  38118  sbcalf  38449  sbcexf  38450  sbccom2  38460  sbccom2f  38461  sbccom2fi  38462  csbcom2fi  38463  anan  38570  br1cnvinxp  38594  idinxpssinxp2  38659  ineleq  38689  brabidgaw  38708  brabidga  38709  inxpxrn  38753  rnxrn  38756  dfsucmap3  38798  cossssid2  38893  cossssid3  38894  cosscnvssid3  38901  dfeldisj3  39146  dfeldisj4  39147  antisymrelres  39201  dfmembpart2  39208  mpet3  39285  cpet2  39286  prtlem70  39317  prtlem16  39329  ishlat2  39813  pmapglb  40230  polval2N  40366  dicelval3  41640  mapdordlem1a  42094  redvmptabs  42806  fimgmcyclem  42992  fimgmcyc  42993  prjspeclsp  43059  sn-isghm  43120  abbibw  43124  fz1eqin  43215  7rexfrabdioph  43246  rmydioph  43460  dford4  43475  areaquad  43662  onsupmaxb  43685  onov0suclim  43720  nnoeomeqom  43758  tfsconcat0i  43791  faosnf0.11b  43872  ifpan23  43905  ifpdfnan  43931  ifpdfxor  43932  ifpidg  43936  ifpid1g  43939  ifpim123g  43945  ifp1bi  43947  ifpimimb  43949  ifpororb  43950  ifpbibib  43955  rp-fakeuninass  43961  dfsucon  43968  minregex  43979  cllem0  44011  rababg  44019  elmapintrab  44021  elmapintab  44041  undmrnresiss  44049  dfxor4  44211  dfhe3  44220  dffrege115  44423  frege131  44439  frege133  44441  clsk1indlem4  44489  clsk1indlem1  44490  expandrexn  44736  rr-groth  44744  rr-grothshortbi  44748  undisjrab  44751  pm13.196a  44859  eelT11  45151  eelTT1  45154  eelT01  45155  eel0T1  45156  uunTT1  45237  uunTT1p1  45238  uunTT1p2  45239  uunT11  45240  uunT11p1  45241  uunT11p2  45242  uun111  45249  xpwf  45409  permaxinf2lem  45457  permac8prim  45459  ssrabf  45562  rabssf  45567  disjinfi  45640  elicores  45981  fourierdlem42  46595  iundjiun  46906  2reu7  47571  2reu8  47572  2reu8i  47573  dfdfat2  47588  aovov0bi  47656  afv2orxorb  47688  afv2ndeffv0  47720  ichcircshi  47926  ichan  47927  icheq  47934  ichal  47938  prpair  47973  prproropf1olem0  47974  257prm  48036  fmtno4prmfac  48047  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  clnbgrel  48316  isubgr3stgrlem4  48457  usgrexmpl2nb1  48520  usgrexmpl2nb2  48521  gpgprismgr4cycllem10  48592  uspgrsprf1  48635  rrx2xpref1o  49206  iinxp  49318  resinsn  49359  resinsnALT  49360  0funcALT  49575  catcsect  49885  isthincd2  49924  aacllem  50288