Theorem 3bitri 286

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
3bitri.1	|- ( ph <-> ps )
3bitri.2	|- ( ps <-> ch )
3bitri.3	|- ( ch <-> th )

Assertion

Ref	Expression
3bitri	|- ( ph <-> th )

Proof of Theorem 3bitri

Step	Hyp	Ref	Expression
1		3bitri.1	. 2 |- ( ph <-> ps )
2		3bitri.2	. . 3 |- ( ps <-> ch )
3		3bitri.3	. . 3 |- ( ch <-> th )
4	2, 3	bitri 264	. 2 |- ( ps <-> th )
5	1, 4	bitri 264	1 |- ( ph <-> th )

Syntax hints:   <-> wb 196

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 197

This theorem is referenced by:  bibi1i  328  orbi1i  542  orass  546  or32  549  pm5.32  668  an32  839  cases  992  an3andi  1445  an33rean  1446  nanbi  1454  excxor  1469  cadan  1548  cadcomb  1552  nic-axALT  1599  tbw-bijust  1623  rb-bijust  1674  nf2  1711  19.43  1810  19.43OLD  1811  19.12vvv  1907  3exdistr  1923  excom13  2044  19.12vv  2180  eeeanv  2183  ee4anv  2184  sbn  2391  sb3an  2400  sbnf2  2439  sbcom2  2445  sbel2x  2459  sbco4  2466  2sb8e  2467  mo2v  2477  sb8eu  2503  2mo2  2550  2eu7  2559  2eu8  2560  r19.23v  3023  r19.26-3  3066  ralcom13  3100  rexcom13  3101  cbvreu  3169  ceqsralt  3229  ceqsex2  3244  ceqsex4v  3247  ralrab2  3372  rexrab2  3374  reu2  3394  rmo4  3399  reu8  3402  2reu5lem3  3415  sbc3an  3494  reu8nf  3516  rmo2  3526  rmo3  3528  dfss2  3591  ss2rab  3678  rabss  3679  ssrab  3680  dfss4  3858  undi  3874  undif3  3888  undif3OLD  3889  difin2  3890  dfnul2  3917  difin0ss  3946  disj  4017  disj4  4025  rabsssn  4215  disjsn  4246  raldifsni  4324  ssunpr  4365  sspr  4366  sstp  4367  uni0b  4463  uni0c  4464  ssint  4493  iunss  4561  iundif2  4587  disjor  4634  reusv2lem4  4872  nfnid  4897  ssextss  4922  eqvinop  4955  opcom  4965  opeqsn  4967  opeqpr  4968  brabsb  4986  opelopabf  5000  dfid3  5025  pofun  5051  opeliunxp  5170  xpiundi  5173  brinxp2  5180  ssrelOLD  5208  reliun  5239  exopxfr  5265  cnvuni  5309  dmopab3  5337  opelres  5401  elres  5435  elsnres  5436  restidsing  5458  asymref2  5513  intirr  5514  xpeq0  5554  xpdifid  5562  ssrnres  5572  dminxp  5574  dfrel4v  5584  dmsnn0  5600  rnco  5641  coeq0  5644  sspred  5688  wfi  5713  sb8iota  5858  dffun2  5898  fun11  5963  isarep1  5977  dff1o4  6145  opabiota  6261  fvopab5  6309  fvn0ssdmfun  6350  fnressn  6425  f13dfv  6530  dff1o6  6531  fliftel  6559  oprabid  6677  mpt22eqb  6769  ralrnmpt2  6775  uniuni  6971  dflim3  7047  dfom2  7067  elxp4  7110  elxp5  7111  opabex3d  7145  opabex3  7146  el2xptp  7211  xporderlem  7288  dfrecs3  7469  tz7.48lem  7536  seqomlem2  7546  oaord  7627  oeeu  7683  nnaord  7699  ecid  7812  mptelixpg  7945  elixpsn  7947  mapsnen  8035  xpsnen  8044  xpcomco  8050  xpassen  8054  omxpenlem  8061  dom0  8088  modom  8161  tz9.12lem3  8652  rankxpsuc  8745  cp  8754  cardprclem  8805  infxpenlem  8836  dfac5lem1  8946  dfac5lem2  8947  dfac5lem5  8950  dfac10c  8960  kmlem3  8974  kmlem12  8983  kmlem13  8984  kmlem14  8985  kmlem15  8986  ackbij2  9065  cflim2  9085  dffin7-2  9220  dfacfin7  9221  fin1a2lem12  9233  axdc3lem3  9274  cfpwsdom  9406  recmulnq  9786  genpass  9831  psslinpr  9853  suplem2pr  9875  opelreal  9951  ltxrlt  10108  addid1  10216  fimaxre  10968  elnn0  11294  elxnn0  11365  elnn0z  11390  nnwos  11755  elxr  11950  xrnepnf  11952  elfzuzb  12336  4fvwrd4  12459  preduz  12461  elfzo2  12473  ssnn0fi  12784  sqeqori  12976  xpcogend  13713  cotr2g  13715  fsumcom2  14505  fsumcom2OLD  14506  modfsummod  14526  fprodcom2  14714  fprodcom2OLD  14715  rpnnen2lem12  14954  gcdcllem1  15221  isprm2  15395  isprm7  15420  pythagtriplem2  15522  infpn2  15617  4sqlem12  15660  initoid  16655  termoid  16656  eldmcoa  16715  oduposb  17136  gsumwspan  17383  isnsg2  17624  isnsg4  17637  efgcpbllemb  18168  dmdprd  18397  dprdval  18402  dprdw  18409  dprd2d2  18443  dfrhm2  18717  brric2  18745  issubrg  18780  islmim  19062  lbsextlem2  19159  opsrtoslem1  19484  cnfldfunALT  19759  pjfval2  20053  fvmptnn04if  20654  ntreq0  20881  cmpcov2  21193  cmpsub  21203  2ndcdisj  21259  unisngl  21330  txbas  21370  elpt  21375  txkgen  21455  xkococn  21463  fbun  21644  trfil2  21691  fin1aufil  21736  alexsubALTlem3  21853  cnextcn  21871  qustgplem  21924  eltsms  21936  ustn0  22024  fmucndlem  22095  metrest  22329  restmetu  22375  isclmp  22897  srabn  23156  ellogdm  24385  1cubr  24569  leibpilem2  24668  dmarea  24684  vmasum  24941  dchrelbas2  24962  2lgslem4  25131  tgcgr4  25426  ltgov  25492  axlowdimlem13  25834  axeuclidlem  25842  numedglnl  26039  nbgrel  26238  nbupgrres  26266  vtxd0nedgb  26384  rusgrprc  26486  usgr2pth0  26661  isclwwlks  26880  clwwlksn2  26910  3pthdlem1  27024  iseupthf1o  27062  frgr3v  27139  fusgr2wsp2nb  27198  frgrregord013  27253  h2hcau  27836  h2hlm  27837  axhcompl-zf  27855  shlesb1i  28245  shne0i  28307  chnlei  28344  cmbr2i  28455  pjneli  28582  ho02i  28688  adjsym  28692  adjeu  28748  lnopeqi  28867  largei  29126  atoml2i  29242  cdj3lem3b  29299  or3di  29307  mo5f  29324  rmo3f  29335  rmo4fOLD  29336  disjnf  29384  disjorf  29392  ssrelf  29425  ofpreima  29465  disjdsct  29480  1stpreima  29484  2ndpreima  29485  f1od2  29499  xrdifh  29542  nndiffz1  29548  ordtconnlem1  29970  ind1a  30081  measiuns  30280  elunirnmbfm  30315  eulerpartlemr  30436  eulerpartlemgh  30440  eulerpartlemn  30443  ballotlemodife  30559  bnj250  30767  bnj334  30779  bnj345  30780  bnj89  30787  bnj115  30791  bnj919  30837  bnj1304  30890  bnj92  30932  bnj124  30941  bnj126  30943  bnj154  30948  bnj155  30949  bnj523  30957  bnj526  30958  bnj540  30962  bnj581  30978  bnj916  31003  bnj929  31006  bnj964  31013  bnj978  31019  bnj983  31021  bnj1039  31039  bnj1040  31040  bnj1123  31054  bnj1128  31058  bnj1398  31102  cvmlift2lem1  31284  elmthm  31473  quad3  31564  3orit  31596  brtp  31639  dftr6  31640  dfpo2  31645  eldm3  31651  elrn3  31652  elima4  31679  19.12b  31707  frind  31740  nosupbnd1lem4  31857  nosupbnd2lem1  31861  slenlt  31877  madeval2  31936  brtxp  31987  brtxp2  31988  brpprod  31992  brpprod3a  31993  elfix  32010  dffix2  32012  ellimits  32017  dffun10  32021  elfuns  32022  elsingles  32025  brimg  32044  brapply  32045  brsuccf  32048  funpartlem  32049  brrestrict  32056  dfrecs2  32057  dfrdg4  32058  brlb  32062  altopthc  32078  altopthd  32079  fvtransport  32139  hfext  32290  nn0prpw  32318  filnetlem4  32376  df3nandALT2  32397  bj-ssbn  32641  bj-cleljustab  32847  bj-sbeq  32896  bj-csbsnlem  32898  bj-elsngl  32956  bj-eltag  32965  bj-tagex  32975  bj-projun  32982  bj-disj2r  33013  bj-restuni  33050  bj-eldiag  33091  bj-eldiag2  33092  topdifinffinlem  33195  relowlpssretop  33212  phpreu  33393  poimirlem24  33433  poimirlem26  33435  poimirlem30  33439  areacirclem5  33504  isbnd2  33582  sbcalf  33917  sbcexf  33918  sbccom2  33930  sbccom2f  33931  sbccom2fi  33932  csbcom2fi  33934  anan  33999  brinxp2ALTV  34034  idinxpssinxp2  34089  ineleq  34119  bropabid  34128  prtlem70  34141  prtlem16  34154  ishlat2  34640  polval2N  35192  dicelval3  36469  mapdordlem1a  36923  fz1eqin  37332  7rexfrabdioph  37364  rmydioph  37581  dford4  37596  areaquad  37802  ifpan23  37804  ifpdfnan  37831  ifpdfxor  37832  ifpidg  37836  ifpid1g  37839  ifpim123g  37845  ifp1bi  37847  ifpimimb  37849  ifpororb  37850  ifpbibib  37855  rp-fakenanass  37860  rp-fakeuninass  37862  cllem0  37871  rababg  37879  elmapintrab  37882  elmapintab  37902  undmrnresiss  37910  ss2iundf  37951  dfxor4  38058  rp-imass  38065  dfhe3  38069  dffrege115  38272  frege131  38288  frege133  38290  clsk1indlem4  38342  clsk1indlem1  38343  undisjrab  38505  pm13.196a  38615  eelT11  38932  eelTT1  38935  eelT01  38936  eel0T1  38937  uunTT1  39020  uunTT1p1  39021  uunTT1p2  39022  uunT11  39023  uunT11p1  39024  uunT11p2  39025  uun111  39032  iunssf  39263  ssrabf  39298  rabssf  39302  disjinfi  39380  elicores  39760  fourierdlem42  40366  iundjiun  40677  2reu7  41191  2reu8  41192  dfdfat2  41211  aovov0bi  41276  257prm  41473  fmtno4prmfac  41484  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  uspgrsprf1  41755  opeliun2xp  42111  aacllem  42547