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  686  mt2bi  688  orbi12i  769  or42  777  pm5.53  807  orddi  825  anddi  826  pm2.1dc  842  dcim  846  notnotrdc  848  dcnnOLD  854  rbaib  926  rbaibr  927  pm4.43  955  orbididc  959  pm5.75  968  ifptru  995  ifpfal  996  3orass  1005  3anass  1006  3ancomb  1010  3anan32  1013  3anan12  1014  anandi3  1015  anandi3r  1016  xordc  1434  falbitru  1459  19.26-2  1528  19.26-3an  1529  alrot3  1531  albiim  1533  2albiim  1534  19.27h  1606  19.27  1607  19.28h  1608  19.28  1609  nfalt  1624  aaanh  1632  aaan  1633  alinexa  1649  19.21-2  1713  nf2  1714  19.44  1728  19.45  1729  exrot3  1736  exrot4  1737  eeor  1741  sbcof2  1856  sbid2h  1895  19.23vv  1930  sbnv  1935  sblimv  1941  pm11.53  1942  19.41vv  1950  19.41vvv  1951  19.41vvvv  1952  exdistrv  1957  19.42vv  1958  19.42vvv  1959  19.42vvvv  1960  4exdistr  1963  cbvex4v  1981  eean  1982  sbn  2003  sbim  2004  sbor  2005  sban  2006  sbrim  2007  sblim  2008  sbbi  2010  sblbis  2011  sbrbis  2012  sbrbif  2013  sbco2d  2017  sbco2vd  2018  sbnf2  2032  2sb5  2034  2sb6  2035  sbcom2v  2036  sbcom2v2  2037  sbcom2  2038  sb6a  2039  2sb5rf  2040  2sb6rf  2041  sbalyz  2050  sbal  2051  sbal1yz  2052  sbex  2055  sbalv  2056  sbco4lem  2057  exsb  2059  2exsb  2060  eujust  2079  euf  2082  cbveu  2101  mor  2120  eu2  2122  mo4f  2138  eu4  2140  2exeu  2170  2eu4  2171  exists1  2174  abid  2217  eleq12i  2297  abeq2  2338  abeq2i  2340  clabel  2356  abid2f  2398  sbabel  2399  neeq12i  2417  neanior  2487  ralnex  2518  dfrex2dc  2521  ralinexa  2557  nfraldya  2565  nfrexdya  2566  r3al  2574  r19.26-2  2660  ralbiim  2665  ralnex2  2670  r19.43  2689  ralcomf  2692  rexcomf  2693  ralrot3  2696  rexrot4  2698  reean  2700  3reeanv  2702  rabbi  2709  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvral2vw  2776  cbvrex2vw  2777  cbvral2v  2778  cbvrex2v  2779  cbvral3v  2780  cbvralsv  2781  cbvrexsv  2782  sbralie  2783  rabeq2i  2796  issetf  2807  2gencl  2833  3gencl  2834  ceqsex2  2841  ceqsex3v  2843  ceqsex6v  2845  ceqsex8v  2846  gencbvex  2847  gencbval  2849  spc2gv  2894  eqvincf  2928  ceqsrex2v  2935  clel5  2940  elrab2  2962  ralab  2963  ralrab  2964  rexab  2965  rexrab  2966  ralab2  2967  rexab2  2969  eueq3dc  2977  morex  2987  euind  2990  reu2  2991  reu6  2992  rmo4  2996  reu4  2997  reu7  2998  rmo3f  3000  rmo4f  3001  rmoim  3004  2reuswapdc  3007  reuind  3008  2rmorex  3009  sbcco  3050  sbccomlem  3103  sbccom  3104  ra5  3118  rmo3  3121  csbco  3134  csbcow  3135  sbnfc2  3185  csbabg  3186  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  dfss  3211  dfss2f  3215  ss2ab  3292  dfdif3  3314  difeqri  3324  ddifstab  3336  raldifb  3344  uneqri  3346  ssequn2  3377  unss  3378  rexun  3384  ralunb  3385  elin2  3392  ineqri  3397  dfss1  3408  dfss5  3409  dfss4st  3437  ssddif  3438  difin  3441  indif  3447  difundi  3456  indifdir  3460  symdifxor  3470  inrab2  3477  rabun2  3483  reuun2  3487  0el  3514  rabeq0  3521  abeq0  3522  disjr  3541  disj1  3542  undif4  3554  uneqdifeqim  3577  r19.2m  3578  r19.3rm  3580  r19.9rmv  3583  raaan  3597  pwss  3665  dfpr2  3685  rexdifpr  3694  ralsnsg  3703  ralsns  3704  eltpg  3711  eldiftp  3712  ralprg  3717  rexprg  3718  raltpg  3719  rextpg  3720  snprc  3731  rabrsndc  3734  euabsn2  3735  eusn  3740  eldifsn  3795  ssdifsn  3796  rexdifsn  3800  eqsnm  3833  tpss  3836  snsssn  3839  prel12  3849  preqsn  3853  oprcl  3881  pwtpss  3885  eluniab  3900  elunirab  3901  unipr  3902  dfnfc2  3906  uniun  3907  uniin  3908  uni0b  3913  unissb  3918  elintab  3934  elintrab  3935  ssintab  3940  ssintrab  3946  intun  3954  intpr  3955  elrint  3963  iuncom4  3972  iuneq2  3981  dfiun2g  3997  ssiinf  4015  iundif2ss  4031  elriin  4036  iunxiun  4047  pwssb  4051  elpwpw  4052  iunpwss  4057  dfdisj2  4061  disjiun  4078  cbvopab1  4157  dftr5  4185  trint  4197  inex1  4218  inuni  4240  repizf2lem  4246  unidif0  4252  axpweq  4256  bnd2  4258  exmid01  4283  zfpair2  4295  exss  4314  elop  4318  opm  4321  otth  4329  copsex4g  4334  opeqsn  4340  opelopabsbALT  4348  brabga  4353  opelopabaf  4363  iunopab  4371  pwunss  4375  pocl  4395  frirrg  4442  elsuci  4495  elsucg  4496  sucel  4502  unisucg  4506  uniuni  4543  reusv3  4552  iunpw  4572  setindel  4631  elirr  4634  en2lp  4647  ordpwsucss  4660  zfregfr  4667  tfi  4675  peano2  4688  peano5  4691  elxp  4737  opelxp  4750  brxp  4751  rabxp  4758  opthprc  4772  brab2a  4774  opeliunxp  4776  xpundi  4777  xpundir  4778  elvvv  4784  brinxp  4789  brab2ga  4796  0xp  4801  ssrel2  4811  eqrelrel  4822  reliun  4843  reluni  4845  raliunxp  4866  rexiunxp  4867  ralxpf  4871  rexxpf  4872  iunxpf  4873  relop  4875  elco  4891  elcnv  4902  elcnv2  4903  dmin  4934  dmuni  4936  dmopab  4937  dmi  4941  dmmrnm  4946  rnopab  4974  elrnmpt1  4978  rncoeq  5001  resiexg  5053  restidsing  5064  dfima2  5073  dfima3  5074  elima2  5077  elima3  5078  imai  5087  elimasn  5098  epini  5102  dfse2  5104  cotr  5113  issref  5114  intasym  5116  asymref  5117  cnvopab  5133  cnvi  5136  cnvdif  5138  imainss  5147  rnxpid  5166  dfrel2  5182  dfrel3  5189  dmsnm  5197  rnsnm  5198  relsn2m  5202  dmsnopg  5203  cnvcnvsn  5208  elxp4  5219  elxp5  5220  cnvresima  5221  mptpreima  5225  dfco2  5231  coundi  5233  coundir  5234  imaco  5237  coiun  5241  coi1  5247  relssdmrn  5252  relrelss  5258  unixpm  5267  ressn  5272  cnviinm  5273  cnvpom  5274  cnvsom  5275  cbviota  5286  iotass  5299  eliota  5309  dffun2  5331  dffun4  5332  dffun7  5348  dffun8  5349  dffun9  5350  funopab  5356  funun  5365  funcnvsn  5369  fntpg  5380  funcnv2  5384  funcnv  5385  fun2cnv  5388  fncnv  5390  fun11  5391  fununi  5392  imadiflem  5403  imadif  5404  imainlem  5405  funimaexglem  5407  fnunsn  5433  fnres  5443  fnopabg  5450  mptfng  5452  mptun  5458  fun  5502  fcnvres  5514  dff12  5535  f1cnvcnv  5547  funforn  5560  dff1o2  5582  dff1o5  5586  f1orn  5587  resdif  5599  ffoss  5609  f11o  5610  f1o00  5613  fo00  5614  elfv  5630  fv3  5655  nfvres  5668  eqfnfv3  5739  fneqeql  5748  unpreima  5765  respreima  5768  dffo3  5787  dffo5  5789  f1ompt  5791  ffnfvf  5799  fmptco  5806  funopdmsn  5826  ftpg  5830  fnressn  5832  idref  5889  abrexco  5892  dff13  5901  dff13f  5903  fliftel  5926  isoini  5951  eusvobj2  5996  acexmidlema  6001  acexmidlemb  6002  acexmidlemph  6003  acexmidlem2  6007  oprabid  6042  brabvv  6059  dfoprab2  6060  eqoprab2b  6071  dmoprab  6094  rnoprab  6096  eloprabga  6100  mpomptx  6104  resoprab  6109  ffnov  6117  elrnmpo  6127  ralrnmpo  6128  rexrnmpo  6129  ovid  6130  ovi3  6151  ov6g  6152  foov  6161  opabex3d  6275  opabex3  6276  abexssex  6279  oprabex3  6283  oprabrexex2  6284  fmpo  6358  xporderlem  6388  f1od2  6392  mpoxopovel  6398  brtpos2  6408  dmtpos  6413  tpostpos  6421  tpossym  6433  tposoprab  6437  dfsmo2  6444  tfrlem7  6474  tfrlem9  6476  tfr1onlemaccex  6505  tfrcllemaccex  6518  tfrcldm  6520  frecabex  6555  el1o  6596  dif1o  6597  dfer2  6694  brdifun  6720  eqerlem  6724  qsid  6760  iinerm  6767  riinerm  6768  erinxp  6769  brecop  6785  eroveu  6786  erovlem  6787  ecopovsym  6791  mapval2  6838  mapsn  6850  elixp  6865  ixpeq2  6872  ixpin  6883  ixpiinm  6884  mptelixpg  6894  ixpsnf1o  6896  domen  6913  isfi  6925  en1  6964  xpsnen  6993  xpcomco  6998  xpassen  7002  ssenen  7025  nneneq  7031  snnen2oprc  7034  ac6sfi  7073  exmidpw  7086  exmidpweq  7087  pw1dc1  7092  eldju  7251  djur  7252  eldju2ndl  7255  eldju2ndr  7256  finomni  7323  nninfwlporlemd  7355  nninfwlpoimlemg  7358  acfun  7405  pw1nel3  7432  sucpw1nel3  7434  ccfunen  7466  elni  7511  ltexpi  7540  enq0enq  7634  enq0ref  7636  enq0tr  7637  prarloclem3  7700  ltdfpr  7709  genpdflem  7710  genpassl  7727  genpassu  7728  nqprrnd  7746  nqprl  7754  nqpru  7755  ltexprlemopl  7804  ltexprlemopu  7806  ltexprlemdisj  7809  ltexprlemloc  7810  recexprlemdisj  7833  caucvgprprlemell  7888  caucvgprprlemelu  7889  suplocexprlemml  7919  suplocsrlemb  8009  opelcn  8029  elreal  8031  elreal2  8033  peano1nnnn  8055  axicn  8066  axaddf  8071  axmulf  8072  axprecex  8083  axpre-ltirr  8085  axpre-mulgt0  8090  axcaucvglemres  8102  axpre-suploc  8105  xrlenlt  8227  ltxrlt  8228  inelr  8747  reapcotr  8761  1nn  9137  elnnne0  9399  un0addcl  9418  un0mulcl  9419  elnnz  9472  elznn0nn  9476  elznn0  9477  elznn  9478  elz2  9534  zapne  9537  3halfnz  9560  prime  9562  raluz2  9791  rexuz2  9793  supinfneg  9807  infsupneg  9808  eluz2b2  9815  eluz2b3  9816  ublbneg  9825  elq  9834  qreccl  9854  elpq  9861  ralrp  9888  rexrp  9889  rpnegap  9899  ltxr  9988  xrnemnf  9990  xrltso  10009  icc0r  10139  divelunit  10215  fzprval  10295  fztpval  10296  elfz1b  10303  fz01or  10324  4fvwrd4  10353  fzolb  10367  fzolb2  10368  elfzo3  10377  fzouzsplit  10394  elfzo0z  10401  fzo0m  10409  fzind2  10462  ioo0  10496  ico0  10498  ioc0  10499  uzennn  10675  seq3f1olemp  10754  iswrd  11091  caucvgre  11513  cvg1nlemcau  11516  resqrexlemex  11557  climeu  11828  fsum2dlemstep  11966  expcnv  12036  prodsnf  12124  fprod2dlemstep  12154  divides  12321  m1exp1  12433  divalgb  12457  bitsval2  12476  bitsmod  12488  bitscmp  12490  bezoutlemnewy  12538  bezoutlemmain  12540  bezoutlemex  12543  dfgcd2  12556  nnwosdc  12581  lcmgcdlem  12620  isprm2  12660  isprm3  12661  isprm4  12662  isprm5  12685  sqrt2irr  12705  oddpwdc  12717  pythagtriplem19  12826  pythagtrip  12827  pceu  12839  dvdsprmpweqnn  12880  4sqlem2  12933  4sqlem12  12946  dec5dvds2  12957  ennnfoneleminc  13003  ennnfonelemex  13006  ennnfonelemr  13015  ctiunct  13032  infpn2  13048  xpsfrnel  13398  xpsfrnel2  13400  gsum0g  13450  ismnd  13473  dfgrp2e  13582  dfgrp3me  13654  isnsg2  13761  eqger  13782  isabl2  13852  imasabl  13894  isrhm  14143  isrim  14154  isnzr2  14169  lss1d  14368  istps  14727  istps2  14728  isbasis2g  14740  tgval2  14746  txuni2  14951  tx1cn  14964  tx2cn  14965  uptx  14969  txdis1cn  14973  blres  15129  xmeterval  15130  xmeter  15131  isxms2  15147  isms2  15149  metrest  15201  qtopbasss  15216  dedekindicclemicc  15327  limcdifap  15357  plyrecj  15458  pilem1  15474  sincosq1lem  15520  mpodvdsmulf1o  15685  gausslemma2dlem1a  15758  gausslemma2dlem4  15764  lgsquadlem1  15777  lgsquadlem2  15778  2lgslem1b  15789  2sqlem1  15814  upgrex  15924  griedg0ssusgr  16070  clwwlkn1loopb  16188  decidr  16269  bdcuni  16348  bdcriota  16355  bdinex1  16371  bj-zfpair2  16382  bj-axun2  16387  bj-ssom  16408  ss1oel2o  16464  nninfsellemdc  16490  nninfsellemsuc  16492  nninfsellemqall  16495  trirec0xor  16527  iswomni0  16533