Theorem bitri 184

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)

Hypotheses

Ref	Expression
bitri.1	⊢ (𝜑 ↔ 𝜓)
bitri.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
bitri	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem bitri

Step	Hyp	Ref	Expression
1		bitri.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 120	. . 3 ⊢ (𝜑 → 𝜓)
3		bitri.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
4	2, 3	sylib 122	. 2 ⊢ (𝜑 → 𝜒)
5	3	biimpri 133	. . 3 ⊢ (𝜒 → 𝜓)
6	5, 1	sylibr 134	. 2 ⊢ (𝜒 → 𝜑)
7	4, 6	impbii 126	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bitr2i  185  bitr3i  186  bitr4i  187  bitrd  188  3bitri  206  3bitr2i  208  3bitr3i  210  3bitr4i  212  bibi12i  229  imbi12i  239  pm4.71r  394  biadan2  460  anbi2ci  463  anbi12i  464  anbi12ci  465  bianassc  474  pm5.3  479  an42  593  xchbinx  693  mt2bi  695  orbi12i  776  or42  784  pm5.53  814  orddi  832  anddi  833  pm2.1dc  849  dcim  853  notnotrdc  855  dcnnOLD  861  rbaib  933  rbaibr  934  pm4.43  962  orbididc  966  pm5.75  975  ifptru  1002  ifpfal  1003  3orass  1012  3anass  1013  3ancomb  1017  3anan32  1020  3anan12  1021  anandi3  1022  anandi3r  1023  xordc  1441  falbitru  1466  19.26-2  1535  19.26-3an  1536  alrot3  1538  albiim  1540  2albiim  1541  19.27h  1613  19.27  1614  19.28h  1615  19.28  1616  nfalt  1631  aaanh  1639  aaan  1640  alinexa  1656  19.21-2  1719  nf2  1720  19.44  1734  19.45  1735  exrot3  1742  exrot4  1743  eeor  1747  sbcof2  1863  sbid2h  1902  19.23vv  1937  sbnv  1943  sblimv  1950  pm11.53  1951  19.41vv  1959  19.41vvv  1960  19.41vvvv  1961  exdistrv  1966  19.42vv  1967  19.42vvv  1968  19.42vvvv  1969  4exdistr  1972  cbvex4v  1990  eean  1991  sbn  2012  sbim  2013  sbor  2014  sban  2015  sbrim  2016  sblim  2017  sbbi  2019  sblbis  2020  sbrbis  2021  sbrbif  2022  sbco2d  2026  sbco2vd  2027  sbnf2  2041  2sb5  2043  2sb6  2044  sbcom2v  2045  sbcom2v2  2046  sbcom2  2047  sb6a  2048  2sb5rf  2049  2sb6rf  2050  sbalyz  2059  sbal  2060  sbal1yz  2061  sbex  2064  sbalv  2065  sbco4lem  2066  exsb  2068  2exsb  2069  eujust  2088  euf  2091  cbveu  2110  mor  2129  eu2  2131  mo4f  2147  eu4  2149  2exeu  2179  2eu4  2180  exists1  2183  abid  2226  eleq12i  2306  abeq2  2347  abeq2i  2349  abbib  2356  clabel  2367  eqabb  2374  eqabbw  2375  abid2f  2418  sbabel  2419  neeq12i  2437  neanior  2507  ralnex  2538  dfrex2dc  2541  ralinexa  2577  nfraldya  2585  nfrexdya  2586  r3al  2594  r19.26-2  2680  ralbiim  2685  ralnex2  2690  r19.43  2709  ralcomf  2712  rexcomf  2713  ralrot3  2716  rexrot4  2718  reean  2720  3reeanv  2722  reqabi  2728  rabbi  2730  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvral2vw  2797  cbvrex2vw  2798  cbvral2v  2799  cbvrex2v  2800  cbvral3v  2801  cbvralsv  2802  cbvrexsv  2803  sbralie  2804  rabeq2i  2818  issetf  2829  2gencl  2855  3gencl  2856  ceqsex2  2863  ceqsex3v  2865  ceqsex6v  2867  ceqsex8v  2868  gencbvex  2869  gencbval  2871  spc2gv  2916  eqvincf  2951  ceqsrex2v  2958  clel5  2963  elrab2  2985  ralab  2986  ralrab  2987  rexab  2988  rexrab  2989  ralab2  2990  rexab2  2992  eueq3dc  3000  morex  3010  euind  3013  reu2  3014  reu6  3015  rmo4  3019  reu4  3020  reu7  3021  rmo3f  3023  rmo4f  3024  rmoim  3027  2reuswapdc  3030  reuind  3031  2rmorex  3032  sbcco  3073  sbccomlem  3126  sbccom  3127  ra5  3141  rmo3  3144  csbco  3157  csbcow  3158  sbnfc2  3208  csbabg  3209  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  dfss  3234  dfssf  3238  dfss2f  3239  ss2ab  3316  dfdif3  3339  difeqri  3349  ddifstab  3361  raldifb  3369  uneqri  3371  ssequn2  3402  unss  3403  rexun  3409  ralunb  3410  elin2  3417  ineqri  3424  dfss1  3435  dfss5  3436  dfss4st  3464  ssddif  3465  difin  3468  indif  3474  difundi  3483  indifdir  3487  symdifxor  3497  inrab2  3506  rabun2  3512  reuun2  3516  0el  3544  ab0w  3550  rabeq0  3552  abeq0  3553  disjr  3574  disj1  3575  undif4  3587  uneqdifeqim  3613  r19.2m  3614  r19.3rm  3616  r19.9rmv  3619  raaan  3633  pwss  3707  dfpr2  3727  rexdifpr  3736  ralsnsg  3745  ralsns  3746  eltpg  3753  eldiftp  3754  ralprg  3759  rexprg  3760  raltpg  3761  rextpg  3762  snprc  3773  rabrsndc  3778  euabsn2  3779  eusn  3784  eldifsn  3839  ssdifsn  3840  rexdifsn  3844  eqsnm  3878  tpss  3881  snsssn  3884  prel12  3894  preqsn  3898  oprcl  3926  pwtpss  3930  eluniab  3945  elunirab  3946  unipr  3947  dfnfc2  3951  uniun  3952  uniin  3953  uni0b  3958  unissb  3963  elintab  3979  elintrab  3980  ssintab  3985  ssintrab  3991  intun  3999  intpr  4000  elrint  4008  iuncom4  4017  iuneq2  4026  dfiun2g  4042  ssiinf  4060  iundif2ss  4076  elriin  4081  iunxiun  4092  pwssb  4096  elpwpw  4097  iunpwss  4102  dfdisj2  4106  disjiun  4123  cbvopab1  4202  dftr5  4230  trint  4242  inex1  4265  inuni  4289  repizf2lem  4296  unidif0  4302  axpweq  4306  bnd2  4308  exmid01  4333  zfpair2  4345  exss  4365  elop  4369  opm  4372  otth  4380  copsex4g  4385  opeqsn  4391  opelopabsbALT  4399  brabga  4404  opelopabaf  4414  iunopab  4422  pwunss  4426  pocl  4446  frirrg  4493  elsuci  4546  elsucg  4547  sucel  4553  unisucg  4557  uniuni  4595  reusv3  4604  iunpw  4624  setindel  4683  elirr  4686  en2lp  4699  ordpwsucss  4712  zfregfr  4719  tfi  4727  peano2  4740  peano5  4743  elxp  4789  opelxp  4802  brxp  4803  rabxp  4810  opthprc  4824  brab2a  4826  opeliunxp  4828  xpundi  4829  xpundir  4830  elvvv  4836  brinxp  4841  brab2ga  4848  0xp  4853  ssrel2  4863  eqrelrel  4874  reliun  4896  reluni  4898  raliunxp  4919  rexiunxp  4920  ralxpf  4924  rexxpf  4925  iunxpf  4926  relop  4928  elco  4944  elcnv  4955  elcnv2  4956  dmin  4987  dmuni  4989  dmopab  4990  dmi  4994  dmmrnm  4999  rnopab  5027  elrnmpt1  5031  rncoeq  5054  resiexg  5106  restidsing  5117  dfima2  5126  dfima3  5127  elima2  5130  elima3  5131  imai  5141  elimasn  5152  epini  5156  dfse2  5158  cotr  5167  issref  5168  intasym  5170  asymref  5171  cnvopab  5187  cnvi  5190  cnvdif  5192  imainss  5201  rnxpid  5220  dfrel2  5236  dfrel3  5243  dmsnm  5251  rnsnm  5252  relsn2m  5256  dmsnopg  5257  cnvcnvsn  5262  elxp4  5273  elxp5  5274  cnvresima  5275  mptpreima  5279  dfco2  5285  coundi  5287  coundir  5288  imaco  5291  coiun  5295  coi1  5301  relssdmrn  5306  relrelss  5312  unixpm  5321  ressn  5326  cnviinm  5327  cnvpom  5328  cnvsom  5329  cbviota  5340  iotass  5353  eliota  5363  dffun2  5385  dffun4  5386  dffun7  5402  dffun8  5403  dffun9  5404  funopab  5410  funun  5420  funcnvsn  5424  fntpg  5435  funcnv2  5439  funcnv  5440  fun2cnv  5443  fncnv  5445  fun11  5446  fununi  5447  imadiflem  5458  imadif  5459  imainlem  5460  funimaexglem  5462  fnunsn  5488  fnres  5498  fnopabg  5505  mptfng  5507  mptun  5513  fun  5559  fcnvres  5573  dff12  5595  f1cnvcnv  5607  funforn  5620  dff1o2  5642  dff1o5  5646  f1orn  5647  resdif  5659  ffoss  5670  f11o  5671  f1o00  5674  fo00  5675  elfv  5691  fv3  5716  nfvres  5729  eqfnfv3  5802  fneqeql  5811  unpreima  5827  respreima  5830  dffo3  5849  dffo5  5851  f1ompt  5853  ffnfvf  5861  fmptco  5868  funopdmsn  5889  ftpg  5893  fnressn  5895  idref  5956  abrexco  5959  dff13  5968  dff13f  5970  fliftel  5993  isoini  6018  eusvobj2  6065  acexmidlema  6070  acexmidlemb  6071  acexmidlemph  6072  acexmidlem2  6076  oprabid  6111  brabvv  6128  dfoprab2  6129  eqoprab2b  6140  dmoprab  6163  rnoprab  6165  eloprabga  6169  mpomptx  6173  resoprab  6178  ffnov  6186  elrnmpo  6196  ralrnmpo  6197  rexrnmpo  6198  ovid  6199  ovi3  6220  ov6g  6221  foov  6230  opabex3d  6344  opabex3  6345  abexssex  6348  oprabex3  6356  oprabrexex2  6357  fmpo  6431  xporderlem  6461  f1od2  6465  mpoxopovel  6506  brtpos2  6516  dmtpos  6521  tpostpos  6529  tpossym  6541  tposoprab  6545  dfsmo2  6552  tfrlem7  6582  tfrlem9  6584  tfr1onlemaccex  6613  tfrcllemaccex  6626  tfrcldm  6628  frecabex  6663  el1o  6704  dif1o  6705  dfer2  6802  brdifun  6828  eqerlem  6832  qsid  6868  iinerm  6875  riinerm  6876  erinxp  6877  brecop  6893  eroveu  6894  erovlem  6895  ecopovsym  6899  mapval2  6953  mapsn  6966  elixp  6981  ixpeq2  6988  ixpin  6999  ixpiinm  7000  mptelixpg  7010  ixpsnf1o  7012  domen  7029  isfi  7041  en1  7080  modom2  7103  xpsnen  7113  xpcomco  7118  xpassen  7122  ssenen  7146  nneneq  7152  snnen2oprc  7155  ac6sfi  7196  exmidpw  7209  exmidpweq  7210  pw1dc1  7215  elfpw  7256  eldju  7402  djur  7403  eldju2ndl  7406  eldju2ndr  7407  finomni  7474  nninfwlporlemd  7506  nninfwlpoimlemg  7509  acfun  7557  pw1nel3  7584  sucpw1nel3  7586  ccfunen  7624  elni  7669  ltexpi  7698  enq0enq  7792  enq0ref  7794  enq0tr  7795  prarloclem3  7858  ltdfpr  7867  genpdflem  7868  genpassl  7885  genpassu  7886  nqprrnd  7904  nqprl  7912  nqpru  7913  ltexprlemopl  7962  ltexprlemopu  7964  ltexprlemdisj  7967  ltexprlemloc  7968  recexprlemdisj  7991  caucvgprprlemell  8046  caucvgprprlemelu  8047  suplocexprlemml  8077  suplocsrlemb  8167  opelcn  8187  elreal  8189  elreal2  8191  peano1nnnn  8213  axicn  8224  axaddf  8229  axmulf  8230  axprecex  8241  axpre-ltirr  8243  axpre-mulgt0  8248  axcaucvglemres  8260  axpre-suploc  8263  xrlenlt  8384  ltxrlt  8385  inelr  8906  reapcotr  8920  1nn  9298  elnnne0  9560  un0addcl  9579  un0mulcl  9580  elnnz  9637  elznn0nn  9641  elznn0  9642  elznn  9643  elz2  9699  zapne  9702  3halfnz  9726  prime  9728  raluz2  9962  rexuz2  9964  supinfneg  9978  infsupneg  9979  eluz2b2  9986  eluz2b3  9987  ublbneg  9996  elq  10005  qreccl  10025  elpq  10032  ralrp  10059  rexrp  10060  rpnegap  10070  ltxr  10160  xrnemnf  10162  xrltso  10181  icc0r  10311  divelunit  10387  fzprval  10472  fztpval  10473  elfz1b  10480  fz01or  10501  4fvwrd4  10530  fzolb  10544  fzolb2  10545  elfzo3  10554  fzouzsplit  10571  elfzo0z  10579  fzo0m  10587  fzind2  10641  infssfzcldc  10652  infssfzledc  10653  ioo0  10677  ico0  10679  ioc0  10680  uzennn  10856  seq3f1olemp  10935  sseqn  11262  hashfibc  11266  hashf1lem2  11269  iswrd  11289  caucvgre  11730  cvg1nlemcau  11733  resqrexlemex  11774  climeu  12045  fsum2dlemstep  12184  expcnv  12254  prodsnf  12342  fprod2dlemstep  12372  divides  12539  m1exp1  12651  divalgb  12675  bitsval2  12694  bitsmod  12706  bitscmp  12708  bezoutlemnewy  12756  bezoutlemmain  12758  bezoutlemex  12761  dfgcd2  12774  nnwosdc  12799  lcmgcdlem  12838  isprm2  12878  isprm3  12879  isprm4  12880  isprm5  12903  sqrt2irr  12923  oddpwdc  12935  pythagtriplem19  13044  pythagtrip  13045  pceu  13057  dvdsprmpweqnn  13098  4sqlem2  13151  4sqlem12  13164  dec5dvds2  13175  ballotfilemodife  13223  ballotfilem4  13224  ennnfoneleminc  13285  ennnfonelemex  13288  ennnfonelemr  13297  ctiunct  13314  infpn2  13330  xpsfrnel  13648  xpsfrnel2  13650  gzsum0  13696  ismnd  13715  dfgrp2e  13816  dfgrp3me  13888  isnsg2  13989  eqger  14010  isabl2  14080  imasabl  14123  isrhm  14448  isrim  14459  isnzr2  14474  drngprop  14600  lss1d  14703  istps  15116  istps2  15117  isbasis2g  15129  tgval2  15135  txuni2  15340  tx1cn  15353  tx2cn  15354  uptx  15358  txdis1cn  15362  blres  15518  xmeterval  15519  xmeter  15520  isxms2  15536  isms2  15538  metrest  15590  qtopbasss  15605  dedekindicclemicc  15716  limcdifap  15746  plyrecj  15847  pilem1  15863  sincosq1lem  15909  mpodvdsmulf1o  16087  gausslemma2dlem1a  16160  gausslemma2dlem4  16166  lgsquadlem1  16179  lgsquadlem2  16180  2lgslem1b  16191  2sqlem1  16216  upgrex  16327  griedg0ssusgr  16475  clwwlkn1loopb  16644  clwwlknon2x  16659  decidr  16807  bdcuni  16885  bdcriota  16892  bdinex1  16908  bj-zfpair2  16919  bj-axun2  16924  bj-ssom  16945  ss1oel2o  17000  nninfsellemdc  17027  nninfsellemsuc  17029  nninfsellemqall  17032  trirec0xor  17068  iswomni0  17075  alsralrex  17127  alsraln0m  17128  2alsraln0m  17132  2alsraln0idm  17133