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  390  biadan2  456  anbi2ci  459  anbi12i  460  anbi12ci  461  bianassc  470  pm5.3  475  an42  587  xchbinx  683  mt2bi  685  orbi12i  765  or42  773  pm5.53  803  orddi  821  anddi  822  pm2.1dc  838  dcim  842  notnotrdc  844  dcnnOLD  850  rbaib  922  rbaibr  923  pm4.43  951  orbididc  955  pm5.75  964  3orass  983  3anass  984  3ancomb  988  3anan32  991  3anan12  992  anandi3  993  anandi3r  994  xordc  1403  falbitru  1428  19.26-2  1496  19.26-3an  1497  alrot3  1499  albiim  1501  2albiim  1502  19.27h  1574  19.27  1575  19.28h  1576  19.28  1577  nfalt  1592  aaanh  1600  aaan  1601  alinexa  1617  19.21-2  1681  nf2  1682  19.44  1696  19.45  1697  exrot3  1704  exrot4  1705  eeor  1709  sbcof2  1824  sbid2h  1863  19.23vv  1898  sbnv  1903  sblimv  1909  pm11.53  1910  19.41vv  1918  19.41vvv  1919  19.41vvvv  1920  exdistrv  1925  19.42vv  1926  19.42vvv  1927  19.42vvvv  1928  4exdistr  1931  cbvex4v  1949  eean  1950  sbn  1971  sbim  1972  sbor  1973  sban  1974  sbrim  1975  sblim  1976  sbbi  1978  sblbis  1979  sbrbis  1980  sbrbif  1981  sbco2d  1985  sbco2vd  1986  sbnf2  2000  2sb5  2002  2sb6  2003  sbcom2v  2004  sbcom2v2  2005  sbcom2  2006  sb6a  2007  2sb5rf  2008  2sb6rf  2009  sbalyz  2018  sbal  2019  sbal1yz  2020  sbex  2023  sbalv  2024  sbco4lem  2025  exsb  2027  2exsb  2028  eujust  2047  euf  2050  cbveu  2069  mor  2087  eu2  2089  mo4f  2105  eu4  2107  2exeu  2137  2eu4  2138  exists1  2141  abid  2184  eleq12i  2264  abeq2  2305  abeq2i  2307  clabel  2323  abid2f  2365  sbabel  2366  neeq12i  2384  neanior  2454  ralnex  2485  dfrex2dc  2488  ralinexa  2524  nfraldya  2532  nfrexdya  2533  r3al  2541  r19.26-2  2626  ralbiim  2631  ralnex2  2636  r19.43  2655  ralcomf  2658  rexcomf  2659  ralrot3  2662  rexrot4  2664  reean  2666  3reeanv  2668  rabbi  2675  cbvralf  2721  cbvrexf  2722  cbvreu  2727  cbvral2vw  2740  cbvrex2vw  2741  cbvral2v  2742  cbvrex2v  2743  cbvral3v  2744  cbvralsv  2745  cbvrexsv  2746  sbralie  2747  rabeq2i  2760  issetf  2770  2gencl  2796  3gencl  2797  ceqsex2  2804  ceqsex3v  2806  ceqsex6v  2808  ceqsex8v  2809  gencbvex  2810  gencbval  2812  spc2gv  2855  eqvincf  2889  ceqsrex2v  2896  clel5  2901  elrab2  2923  ralab  2924  ralrab  2925  rexab  2926  rexrab  2927  ralab2  2928  rexab2  2930  eueq3dc  2938  morex  2948  euind  2951  reu2  2952  reu6  2953  rmo4  2957  reu4  2958  reu7  2959  rmo3f  2961  rmo4f  2962  rmoim  2965  2reuswapdc  2968  reuind  2969  2rmorex  2970  sbcco  3011  sbccomlem  3064  sbccom  3065  ra5  3078  rmo3  3081  csbco  3094  csbcow  3095  sbnfc2  3145  csbabg  3146  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  dfss  3171  dfss2f  3175  ss2ab  3252  dfdif3  3274  difeqri  3284  ddifstab  3296  raldifb  3304  uneqri  3306  ssequn2  3337  unss  3338  rexun  3344  ralunb  3345  elin2  3352  ineqri  3357  dfss1  3368  dfss5  3369  dfss4st  3397  ssddif  3398  difin  3401  indif  3407  difundi  3416  indifdir  3420  symdifxor  3430  inrab2  3437  rabun2  3443  reuun2  3447  0el  3474  rabeq0  3481  abeq0  3482  disjr  3501  disj1  3502  undif4  3514  uneqdifeqim  3537  r19.2m  3538  r19.3rm  3540  r19.9rmv  3543  raaan  3557  pwss  3622  dfpr2  3642  rexdifpr  3651  ralsnsg  3660  ralsns  3661  eltpg  3668  eldiftp  3669  ralprg  3674  rexprg  3675  raltpg  3676  rextpg  3677  snprc  3688  rabrsndc  3691  euabsn2  3692  eusn  3697  eldifsn  3750  ssdifsn  3751  rexdifsn  3755  eqsnm  3786  tpss  3789  snsssn  3792  prel12  3802  preqsn  3806  oprcl  3833  pwtpss  3837  eluniab  3852  elunirab  3853  unipr  3854  dfnfc2  3858  uniun  3859  uniin  3860  uni0b  3865  unissb  3870  elintab  3886  elintrab  3887  ssintab  3892  ssintrab  3898  intun  3906  intpr  3907  elrint  3915  iuncom4  3924  iuneq2  3933  dfiun2g  3949  ssiinf  3967  iundif2ss  3983  elriin  3988  iunxiun  3999  pwssb  4003  elpwpw  4004  iunpwss  4009  dfdisj2  4013  disjiun  4029  cbvopab1  4107  dftr5  4135  trint  4147  inex1  4168  inuni  4189  repizf2lem  4195  unidif0  4201  axpweq  4205  bnd2  4207  exmid01  4232  zfpair2  4244  exss  4261  elop  4265  opm  4268  otth  4276  copsex4g  4281  opeqsn  4286  opelopabsbALT  4294  brabga  4299  opelopabaf  4309  iunopab  4317  pwunss  4319  pocl  4339  frirrg  4386  elsuci  4439  elsucg  4440  sucel  4446  unisucg  4450  uniuni  4487  reusv3  4496  iunpw  4516  setindel  4575  elirr  4578  en2lp  4591  ordpwsucss  4604  zfregfr  4611  tfi  4619  peano2  4632  peano5  4635  elxp  4681  opelxp  4694  brxp  4695  rabxp  4701  opthprc  4715  brab2a  4717  opeliunxp  4719  xpundi  4720  xpundir  4721  elvvv  4727  brinxp  4732  brab2ga  4739  0xp  4744  ssrel2  4754  eqrelrel  4765  reliun  4785  reluni  4787  raliunxp  4808  rexiunxp  4809  ralxpf  4813  rexxpf  4814  iunxpf  4815  relop  4817  elco  4833  elcnv  4844  elcnv2  4845  dmin  4875  dmuni  4877  dmopab  4878  dmi  4882  dmmrnm  4886  rnopab  4914  elrnmpt1  4918  rncoeq  4940  resiexg  4992  restidsing  5003  dfima2  5012  dfima3  5013  elima2  5016  elima3  5017  imai  5026  elimasn  5037  epini  5041  dfse2  5043  cotr  5052  issref  5053  intasym  5055  asymref  5056  cnvopab  5072  cnvi  5075  cnvdif  5077  imainss  5086  rnxpid  5105  dfrel2  5121  dfrel3  5128  dmsnm  5136  rnsnm  5137  relsn2m  5141  dmsnopg  5142  cnvcnvsn  5147  elxp4  5158  elxp5  5159  cnvresima  5160  mptpreima  5164  dfco2  5170  coundi  5172  coundir  5173  imaco  5176  coiun  5180  coi1  5186  relssdmrn  5191  relrelss  5197  unixpm  5206  ressn  5211  cnviinm  5212  cnvpom  5213  cnvsom  5214  cbviota  5225  iotass  5237  eliota  5247  dffun2  5269  dffun4  5270  dffun7  5286  dffun8  5287  dffun9  5288  funopab  5294  funun  5303  funcnvsn  5304  fntpg  5315  funcnv2  5319  funcnv  5320  fun2cnv  5323  fncnv  5325  fun11  5326  fununi  5327  imadiflem  5338  imadif  5339  imainlem  5340  funimaexglem  5342  fnunsn  5368  fnres  5377  fnopabg  5384  mptfng  5386  mptun  5392  fun  5433  fcnvres  5444  dff12  5465  f1cnvcnv  5477  funforn  5490  dff1o2  5512  dff1o5  5516  f1orn  5517  resdif  5529  ffoss  5539  f11o  5540  f1o00  5542  fo00  5543  elfv  5559  fv3  5584  nfvres  5595  eqfnfv3  5664  fneqeql  5673  unpreima  5690  respreima  5693  dffo3  5712  dffo5  5714  f1ompt  5716  ffnfvf  5724  fmptco  5731  ftpg  5749  fnressn  5751  idref  5806  abrexco  5809  dff13  5818  dff13f  5820  fliftel  5843  isoini  5868  eusvobj2  5911  acexmidlema  5916  acexmidlemb  5917  acexmidlemph  5918  acexmidlem2  5922  oprabid  5957  brabvv  5972  dfoprab2  5973  eqoprab2b  5984  dmoprab  6007  rnoprab  6009  eloprabga  6013  mpomptx  6017  resoprab  6022  ffnov  6030  elrnmpo  6040  ralrnmpo  6041  rexrnmpo  6042  ovid  6043  ovi3  6064  ov6g  6065  foov  6074  opabex3d  6187  opabex3  6188  abexssex  6191  oprabex3  6195  oprabrexex2  6196  fmpo  6268  xporderlem  6298  f1od2  6302  mpoxopovel  6308  brtpos2  6318  dmtpos  6323  tpostpos  6331  tpossym  6343  tposoprab  6347  dfsmo2  6354  tfrlem7  6384  tfrlem9  6386  tfr1onlemaccex  6415  tfrcllemaccex  6428  tfrcldm  6430  frecabex  6465  el1o  6504  dif1o  6505  dfer2  6602  brdifun  6628  eqerlem  6632  qsid  6668  iinerm  6675  riinerm  6676  erinxp  6677  brecop  6693  eroveu  6694  erovlem  6695  ecopovsym  6699  mapval2  6746  mapsn  6758  elixp  6773  ixpeq2  6780  ixpin  6791  ixpiinm  6792  mptelixpg  6802  ixpsnf1o  6804  domen  6819  isfi  6829  en1  6867  xpsnen  6889  xpcomco  6894  xpassen  6898  ssenen  6921  nneneq  6927  snnen2oprc  6930  ac6sfi  6968  exmidpw  6978  exmidpweq  6979  pw1dc1  6984  eldju  7143  djur  7144  eldju2ndl  7147  eldju2ndr  7148  finomni  7215  nninfwlporlemd  7247  nninfwlpoimlemg  7250  acfun  7290  pw1nel3  7314  sucpw1nel3  7316  ccfunen  7347  elni  7392  ltexpi  7421  enq0enq  7515  enq0ref  7517  enq0tr  7518  prarloclem3  7581  ltdfpr  7590  genpdflem  7591  genpassl  7608  genpassu  7609  nqprrnd  7627  nqprl  7635  nqpru  7636  ltexprlemopl  7685  ltexprlemopu  7687  ltexprlemdisj  7690  ltexprlemloc  7691  recexprlemdisj  7714  caucvgprprlemell  7769  caucvgprprlemelu  7770  suplocexprlemml  7800  suplocsrlemb  7890  opelcn  7910  elreal  7912  elreal2  7914  peano1nnnn  7936  axicn  7947  axaddf  7952  axmulf  7953  axprecex  7964  axpre-ltirr  7966  axpre-mulgt0  7971  axcaucvglemres  7983  axpre-suploc  7986  xrlenlt  8108  ltxrlt  8109  inelr  8628  reapcotr  8642  1nn  9018  elnnne0  9280  un0addcl  9299  un0mulcl  9300  elnnz  9353  elznn0nn  9357  elznn0  9358  elznn  9359  elz2  9414  zapne  9417  3halfnz  9440  prime  9442  raluz2  9670  rexuz2  9672  supinfneg  9686  infsupneg  9687  eluz2b2  9694  eluz2b3  9695  ublbneg  9704  elq  9713  qreccl  9733  elpq  9740  ralrp  9767  rexrp  9768  rpnegap  9778  ltxr  9867  xrnemnf  9869  xrltso  9888  icc0r  10018  divelunit  10094  fzprval  10174  fztpval  10175  elfz1b  10182  fz01or  10203  4fvwrd4  10232  fzolb  10246  fzolb2  10247  elfzo3  10256  fzouzsplit  10272  elfzo0z  10277  fzo0m  10284  fzind2  10332  ioo0  10366  ico0  10368  ioc0  10369  uzennn  10545  seq3f1olemp  10624  iswrd  10954  caucvgre  11163  cvg1nlemcau  11166  resqrexlemex  11207  climeu  11478  fsum2dlemstep  11616  expcnv  11686  prodsnf  11774  fprod2dlemstep  11804  divides  11971  m1exp1  12083  divalgb  12107  bitsval2  12126  bitsmod  12138  bitscmp  12140  bezoutlemnewy  12188  bezoutlemmain  12190  bezoutlemex  12193  dfgcd2  12206  nnwosdc  12231  lcmgcdlem  12270  isprm2  12310  isprm3  12311  isprm4  12312  isprm5  12335  sqrt2irr  12355  oddpwdc  12367  pythagtriplem19  12476  pythagtrip  12477  pceu  12489  dvdsprmpweqnn  12530  4sqlem2  12583  4sqlem12  12596  dec5dvds2  12607  ennnfoneleminc  12653  ennnfonelemex  12656  ennnfonelemr  12665  ctiunct  12682  infpn2  12698  xpsfrnel  13046  xpsfrnel2  13048  gsum0g  13098  ismnd  13121  dfgrp2e  13230  dfgrp3me  13302  isnsg2  13409  eqger  13430  isabl2  13500  imasabl  13542  isrhm  13790  isrim  13801  isnzr2  13816  lss1d  14015  istps  14352  istps2  14353  isbasis2g  14365  tgval2  14371  txuni2  14576  tx1cn  14589  tx2cn  14590  uptx  14594  txdis1cn  14598  blres  14754  xmeterval  14755  xmeter  14756  isxms2  14772  isms2  14774  metrest  14826  qtopbasss  14841  dedekindicclemicc  14952  limcdifap  14982  plyrecj  15083  pilem1  15099  sincosq1lem  15145  mpodvdsmulf1o  15310  gausslemma2dlem1a  15383  gausslemma2dlem4  15389  lgsquadlem1  15402  lgsquadlem2  15403  2lgslem1b  15414  2sqlem1  15439  decidr  15526  bdcuni  15606  bdcriota  15613  bdinex1  15629  bj-zfpair2  15640  bj-axun2  15645  bj-ssom  15666  ss1oel2o  15722  nninfsellemdc  15741  nninfsellemsuc  15743  nninfsellemqall  15746  trirec0xor  15776  iswomni0  15782