Theorem 3bitri 285

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 263	. 2 ⊢ (𝜓 ↔ 𝜃)
5	1, 4	bitri 263	1 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 195

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 196

This theorem is referenced by:  bibi1i  327  orbi1i  541  orass  545  or32  548  pm5.32  666  an32  835  cases  1004  an3andi  1437  an33rean  1438  nanbi  1446  excxor  1461  cadan  1539  cadcomb  1543  nic-axALT  1590  tbw-bijust  1614  rb-bijust  1665  nf2  1702  19.43  1799  19.43OLD  1800  19.12vvv  1894  3exdistr  1910  excom13  2031  19.12vv  2168  eeeanv  2171  ee4anv  2172  sbn  2379  sb3an  2388  sbnf2  2427  sbcom2  2433  sbel2x  2447  sbco4  2454  2sb8e  2455  mo2v  2465  sb8eu  2491  2mo2  2538  2eu7  2547  2eu8  2548  r19.23v  3005  r19.26-3  3048  rexcom13  3081  cbvreu  3145  ceqsralt  3202  ceqsex2  3217  ceqsex4v  3220  ralrab2  3339  rexrab2  3341  reu2  3361  rmo4  3366  reu8  3369  2reu5lem3  3382  sbc3an  3461  rmo2  3492  rmo3  3494  dfss2  3557  ss2rab  3641  rabss  3642  ssrab  3643  dfss4  3820  undi  3833  undif3  3847  undif3OLD  3848  difin2  3849  dfnul2  3876  difin0ss  3900  disj  3969  disj4  3977  rabsssn  4162  disjsn  4192  raldifsni  4265  ssunpr  4305  sspr  4306  sstp  4307  uni0b  4399  uni0c  4400  ssint  4428  iunss  4497  iundif2  4523  disjor  4567  reusv2lem4  4798  nfnid  4823  ssextss  4849  eqvinop  4881  opcom  4890  opeqsn  4892  opeqpr  4893  brabsb  4911  opelopabf  4925  dfid3  4954  pofun  4975  opeliunxp  5093  xpiundi  5096  brinxp2  5103  ssrelOLD  5131  reliun  5162  exopxfr  5187  cnvuni  5231  dmopab3  5259  opelres  5322  elres  5355  elsnres  5356  restidsing  5377  asymref2  5432  intirr  5433  xpeq0  5473  xpdifid  5481  ssrnres  5491  dminxp  5493  dfrel4v  5503  dmsnn0  5518  rnco  5558  coeq0  5561  sspred  5605  wfi  5630  sb8iota  5775  dffun2  5814  fun11  5877  isarep1  5891  dff1o4  6058  opabiota  6171  fvopab5  6217  fvn0ssdmfun  6258  fnressn  6330  f13dfv  6430  dff1o6  6431  fliftel  6459  oprabid  6576  mpt22eqb  6667  ralrnmpt2  6673  uniuni  6865  dflim3  6939  dfom2  6959  elxp4  7003  elxp5  7004  opabex3d  7037  opabex3  7038  el2xptp  7102  xporderlem  7175  dfrecs3  7356  tz7.48lem  7423  seqomlem2  7433  oaord  7514  oeeu  7570  nnaord  7586  ecid  7699  mptelixpg  7831  elixpsn  7833  mapsnen  7920  xpsnen  7929  xpcomco  7935  xpassen  7939  omxpenlem  7946  dom0  7973  modom  8046  tz9.12lem3  8535  rankxpsuc  8628  cp  8637  cardprclem  8688  infxpenlem  8719  dfac5lem1  8829  dfac5lem2  8830  dfac5lem5  8833  dfac10c  8843  kmlem3  8857  kmlem12  8866  kmlem13  8867  kmlem14  8868  kmlem15  8869  ackbij2  8948  cflim2  8968  dffin7-2  9103  dfacfin7  9104  fin1a2lem12  9116  axdc3lem3  9157  cfpwsdom  9285  recmulnq  9665  genpass  9710  psslinpr  9732  suplem2pr  9754  opelreal  9830  ltxrlt  9987  addid1  10095  fimaxre  10847  elnn0  11171  elxnn0  11242  elnn0z  11267  nnwos  11631  elxr  11826  xrnepnf  11828  elfzuzb  12207  4fvwrd4  12328  preduz  12330  elfzo2  12342  ssnn0fi  12646  sqeqori  12838  xpcogend  13561  cotr2g  13563  fsumcom2  14347  fsumcom2OLD  14348  modfsummod  14367  fprodcom2  14553  fprodcom2OLD  14554  rpnnen2lem12  14793  gcdcllem1  15059  isprm2  15233  isprm7  15258  pythagtriplem2  15360  infpn2  15455  4sqlem12  15498  initoid  16478  termoid  16479  eldmcoa  16538  oduposb  16959  gsumwspan  17206  isnsg2  17447  isnsg4  17460  efgcpbllemb  17991  dmdprd  18220  dprdval  18225  dprdw  18232  dprd2d2  18266  dfrhm2  18540  brric2  18568  issubrg  18603  islmim  18883  lbsextlem2  18980  opsrtoslem1  19305  pjfval2  19872  fvmptnn04if  20473  ntreq0  20691  cmpsub  21013  2ndcdisj  21069  unisngl  21140  txbas  21180  elpt  21185  txkgen  21265  xkococn  21273  fbun  21454  trfil2  21501  fin1aufil  21546  alexsubALTlem3  21663  cnextcn  21681  qustgplem  21734  eltsms  21746  ustn0  21834  fmucndlem  21905  metrest  22139  restmetu  22185  isclmp  22705  srabn  22964  ellogdm  24185  1cubr  24369  leibpilem2  24468  dmarea  24484  vmasum  24741  dchrelbas2  24762  2lgslem4  24931  tgcgr4  25226  ltgov  25292  axlowdimlem13  25634  axeuclidlem  25642  trls  26066  4cycl4v4e  26194  4cycl4dv4e  26196  el2wlkonotot0  26399  usg2spthonot0  26416  frgra3v  26529  usg2spot2nb  26592  frgrareg  26644  frgraregord013  26645  h2hcau  27220  h2hlm  27221  axhcompl-zf  27239  shlesb1i  27629  shne0i  27691  chnlei  27728  cmbr2i  27839  pjneli  27966  ho02i  28072  adjsym  28076  adjeu  28132  lnopeqi  28251  largei  28510  atoml2i  28626  cdj3lem3b  28683  or3di  28691  mo5f  28708  rmo3f  28719  rmo4fOLD  28720  disjnf  28766  disjorf  28774  ssrelf  28805  ofpreima  28848  disjdsct  28863  1stpreima  28867  2ndpreima  28868  f1od2  28887  xrdifh  28932  nndiffz1  28936  ordtconlem1  29298  ind1a  29410  measiuns  29607  elunirnmbfm  29642  eulerpartlemr  29763  eulerpartlemgh  29767  eulerpartlemn  29770  ballotlemodife  29886  bnj250  30020  bnj334  30032  bnj345  30033  bnj89  30041  bnj115  30045  bnj919  30091  bnj1304  30144  bnj92  30186  bnj124  30195  bnj126  30197  bnj154  30202  bnj155  30203  bnj523  30211  bnj526  30212  bnj540  30216  bnj581  30232  bnj916  30257  bnj929  30260  bnj964  30267  bnj978  30273  bnj983  30275  bnj1039  30293  bnj1040  30294  bnj1123  30308  bnj1128  30312  bnj1398  30356  cvmlift2lem1  30538  elmthm  30727  quad3  30818  3orit  30851  brtp  30892  dftr6  30893  dfpo2  30898  eldm3  30905  elrn3  30906  elima4  30924  19.12b  30951  frind  30984  nofulllem5  31105  brtxp  31157  brtxp2  31158  brpprod  31162  brpprod3a  31163  elfix  31180  dffix2  31182  ellimits  31187  dffun10  31191  elfuns  31192  elsingles  31195  brimg  31214  brapply  31215  brsuccf  31218  funpartlem  31219  brrestrict  31226  dfrecs2  31227  dfrdg4  31228  brlb  31232  altopthc  31248  altopthd  31249  fvtransport  31309  hfext  31460  nn0prpw  31488  filnetlem4  31546  df3nandALT2  31567  bj-nf2  31766  bj-ssbn  31830  bj-sbeq  32088  bj-csbsnlem  32090  bj-elsngl  32149  bj-eltag  32158  bj-tagex  32168  bj-projun  32175  bj-restuni  32231  bj-sspwpwab  32239  bj-eldiag  32268  bj-eldiag2  32269  topdifinffinlem  32371  relowlpssretop  32388  phpreu  32563  poimirlem24  32603  poimirlem26  32605  poimirlem30  32609  areacirclem5  32674  isbnd2  32752  sbcalf  33087  sbcexf  33088  sbccom2  33100  sbccom2f  33101  sbccom2fi  33102  csbcom2fi  33104  prtlem70  33157  prtlem16  33172  ishlat2  33658  polval2N  34210  dicelval3  35487  mapdordlem1a  35941  fz1eqin  36350  7rexfrabdioph  36382  rmydioph  36599  dford4  36614  areaquad  36821  ifpan23  36823  ifpdfnan  36850  ifpdfxor  36851  ifpidg  36855  ifpid1g  36858  ifpim123g  36864  ifp1bi  36866  ifpimimb  36868  ifpororb  36869  ifpbibib  36874  rp-fakenanass  36879  rp-fakeuninass  36881  cllem0  36890  rababg  36898  elmapintrab  36901  elmapintab  36921  undmrnresiss  36929  ss2iundf  36970  dfxor4  37077  rp-imass  37085  dfhe3  37089  dffrege115  37292  frege131  37308  frege133  37310  clsk1indlem4  37362  clsk1indlem1  37363  undisjrab  37527  pm13.196a  37637  eelT11  37953  eelTT1  37956  eelT01  37957  eel0T1  37958  uunTT1  38041  uunTT1p1  38042  uunTT1p2  38043  uunT11  38044  uunT11p1  38045  uunT11p2  38046  uun111  38053  inn0f  38268  iunssf  38290  ssrabf  38329  rabssf  38334  disjinfi  38375  elicores  38607  fourierdlem42  39042  iundjiun  39353  2reu7  39840  2reu8  39841  dfdfat2  39860  aovov0bi  39925  257prm  40011  fmtno4prmfac  40022  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  nbgrel  40564  nbupgrres  40592  vtxd0nedgb  40703  rusgrprc  40790  usgr2pth0  40971  isclwwlks  41188  clwwlksn2  41217  3pthdlem1  41331  frgr3v  41445  fusgr2wsp2nb  41498  av-frgraregord013  41549  opeliun2xp  41904  aacllem  42356