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  4239  repizf2lem  4245  unidif0  4251  axpweq  4255  bnd2  4257  exmid01  4282  zfpair2  4294  exss  4313  elop  4317  opm  4320  otth  4328  copsex4g  4333  opeqsn  4339  opelopabsbALT  4347  brabga  4352  opelopabaf  4362  iunopab  4370  pwunss  4374  pocl  4394  frirrg  4441  elsuci  4494  elsucg  4495  sucel  4501  unisucg  4505  uniuni  4542  reusv3  4551  iunpw  4571  setindel  4630  elirr  4633  en2lp  4646  ordpwsucss  4659  zfregfr  4666  tfi  4674  peano2  4687  peano5  4690  elxp  4736  opelxp  4749  brxp  4750  rabxp  4756  opthprc  4770  brab2a  4772  opeliunxp  4774  xpundi  4775  xpundir  4776  elvvv  4782  brinxp  4787  brab2ga  4794  0xp  4799  ssrel2  4809  eqrelrel  4820  reliun  4840  reluni  4842  raliunxp  4863  rexiunxp  4864  ralxpf  4868  rexxpf  4869  iunxpf  4870  relop  4872  elco  4888  elcnv  4899  elcnv2  4900  dmin  4931  dmuni  4933  dmopab  4934  dmi  4938  dmmrnm  4943  rnopab  4971  elrnmpt1  4975  rncoeq  4998  resiexg  5050  restidsing  5061  dfima2  5070  dfima3  5071  elima2  5074  elima3  5075  imai  5084  elimasn  5095  epini  5099  dfse2  5101  cotr  5110  issref  5111  intasym  5113  asymref  5114  cnvopab  5130  cnvi  5133  cnvdif  5135  imainss  5144  rnxpid  5163  dfrel2  5179  dfrel3  5186  dmsnm  5194  rnsnm  5195  relsn2m  5199  dmsnopg  5200  cnvcnvsn  5205  elxp4  5216  elxp5  5217  cnvresima  5218  mptpreima  5222  dfco2  5228  coundi  5230  coundir  5231  imaco  5234  coiun  5238  coi1  5244  relssdmrn  5249  relrelss  5255  unixpm  5264  ressn  5269  cnviinm  5270  cnvpom  5271  cnvsom  5272  cbviota  5283  iotass  5296  eliota  5306  dffun2  5328  dffun4  5329  dffun7  5345  dffun8  5346  dffun9  5347  funopab  5353  funun  5362  funcnvsn  5366  fntpg  5377  funcnv2  5381  funcnv  5382  fun2cnv  5385  fncnv  5387  fun11  5388  fununi  5389  imadiflem  5400  imadif  5401  imainlem  5402  funimaexglem  5404  fnunsn  5430  fnres  5440  fnopabg  5447  mptfng  5449  mptun  5455  fun  5499  fcnvres  5511  dff12  5532  f1cnvcnv  5544  funforn  5557  dff1o2  5579  dff1o5  5583  f1orn  5584  resdif  5596  ffoss  5606  f11o  5607  f1o00  5610  fo00  5611  elfv  5627  fv3  5652  nfvres  5665  eqfnfv3  5736  fneqeql  5745  unpreima  5762  respreima  5765  dffo3  5784  dffo5  5786  f1ompt  5788  ffnfvf  5796  fmptco  5803  funopdmsn  5823  ftpg  5827  fnressn  5829  idref  5886  abrexco  5889  dff13  5898  dff13f  5900  fliftel  5923  isoini  5948  eusvobj2  5993  acexmidlema  5998  acexmidlemb  5999  acexmidlemph  6000  acexmidlem2  6004  oprabid  6039  brabvv  6056  dfoprab2  6057  eqoprab2b  6068  dmoprab  6091  rnoprab  6093  eloprabga  6097  mpomptx  6101  resoprab  6106  ffnov  6114  elrnmpo  6124  ralrnmpo  6125  rexrnmpo  6126  ovid  6127  ovi3  6148  ov6g  6149  foov  6158  opabex3d  6272  opabex3  6273  abexssex  6276  oprabex3  6280  oprabrexex2  6281  fmpo  6353  xporderlem  6383  f1od2  6387  mpoxopovel  6393  brtpos2  6403  dmtpos  6408  tpostpos  6416  tpossym  6428  tposoprab  6432  dfsmo2  6439  tfrlem7  6469  tfrlem9  6471  tfr1onlemaccex  6500  tfrcllemaccex  6513  tfrcldm  6515  frecabex  6550  el1o  6591  dif1o  6592  dfer2  6689  brdifun  6715  eqerlem  6719  qsid  6755  iinerm  6762  riinerm  6763  erinxp  6764  brecop  6780  eroveu  6781  erovlem  6782  ecopovsym  6786  mapval2  6833  mapsn  6845  elixp  6860  ixpeq2  6867  ixpin  6878  ixpiinm  6879  mptelixpg  6889  ixpsnf1o  6891  domen  6908  isfi  6920  en1  6959  xpsnen  6988  xpcomco  6993  xpassen  6997  ssenen  7020  nneneq  7026  snnen2oprc  7029  ac6sfi  7068  exmidpw  7078  exmidpweq  7079  pw1dc1  7084  eldju  7243  djur  7244  eldju2ndl  7247  eldju2ndr  7248  finomni  7315  nninfwlporlemd  7347  nninfwlpoimlemg  7350  acfun  7397  pw1nel3  7424  sucpw1nel3  7426  ccfunen  7458  elni  7503  ltexpi  7532  enq0enq  7626  enq0ref  7628  enq0tr  7629  prarloclem3  7692  ltdfpr  7701  genpdflem  7702  genpassl  7719  genpassu  7720  nqprrnd  7738  nqprl  7746  nqpru  7747  ltexprlemopl  7796  ltexprlemopu  7798  ltexprlemdisj  7801  ltexprlemloc  7802  recexprlemdisj  7825  caucvgprprlemell  7880  caucvgprprlemelu  7881  suplocexprlemml  7911  suplocsrlemb  8001  opelcn  8021  elreal  8023  elreal2  8025  peano1nnnn  8047  axicn  8058  axaddf  8063  axmulf  8064  axprecex  8075  axpre-ltirr  8077  axpre-mulgt0  8082  axcaucvglemres  8094  axpre-suploc  8097  xrlenlt  8219  ltxrlt  8220  inelr  8739  reapcotr  8753  1nn  9129  elnnne0  9391  un0addcl  9410  un0mulcl  9411  elnnz  9464  elznn0nn  9468  elznn0  9469  elznn  9470  elz2  9526  zapne  9529  3halfnz  9552  prime  9554  raluz2  9782  rexuz2  9784  supinfneg  9798  infsupneg  9799  eluz2b2  9806  eluz2b3  9807  ublbneg  9816  elq  9825  qreccl  9845  elpq  9852  ralrp  9879  rexrp  9880  rpnegap  9890  ltxr  9979  xrnemnf  9981  xrltso  10000  icc0r  10130  divelunit  10206  fzprval  10286  fztpval  10287  elfz1b  10294  fz01or  10315  4fvwrd4  10344  fzolb  10358  fzolb2  10359  elfzo3  10368  fzouzsplit  10385  elfzo0z  10392  fzo0m  10400  fzind2  10453  ioo0  10487  ico0  10489  ioc0  10490  uzennn  10666  seq3f1olemp  10745  iswrd  11081  caucvgre  11500  cvg1nlemcau  11503  resqrexlemex  11544  climeu  11815  fsum2dlemstep  11953  expcnv  12023  prodsnf  12111  fprod2dlemstep  12141  divides  12308  m1exp1  12420  divalgb  12444  bitsval2  12463  bitsmod  12475  bitscmp  12477  bezoutlemnewy  12525  bezoutlemmain  12527  bezoutlemex  12530  dfgcd2  12543  nnwosdc  12568  lcmgcdlem  12607  isprm2  12647  isprm3  12648  isprm4  12649  isprm5  12672  sqrt2irr  12692  oddpwdc  12704  pythagtriplem19  12813  pythagtrip  12814  pceu  12826  dvdsprmpweqnn  12867  4sqlem2  12920  4sqlem12  12933  dec5dvds2  12944  ennnfoneleminc  12990  ennnfonelemex  12993  ennnfonelemr  13002  ctiunct  13019  infpn2  13035  xpsfrnel  13385  xpsfrnel2  13387  gsum0g  13437  ismnd  13460  dfgrp2e  13569  dfgrp3me  13641  isnsg2  13748  eqger  13769  isabl2  13839  imasabl  13881  isrhm  14130  isrim  14141  isnzr2  14156  lss1d  14355  istps  14714  istps2  14715  isbasis2g  14727  tgval2  14733  txuni2  14938  tx1cn  14951  tx2cn  14952  uptx  14956  txdis1cn  14960  blres  15116  xmeterval  15117  xmeter  15118  isxms2  15134  isms2  15136  metrest  15188  qtopbasss  15203  dedekindicclemicc  15314  limcdifap  15344  plyrecj  15445  pilem1  15461  sincosq1lem  15507  mpodvdsmulf1o  15672  gausslemma2dlem1a  15745  gausslemma2dlem4  15751  lgsquadlem1  15764  lgsquadlem2  15765  2lgslem1b  15776  2sqlem1  15801  upgrex  15911  decidr  16184  bdcuni  16263  bdcriota  16270  bdinex1  16286  bj-zfpair2  16297  bj-axun2  16302  bj-ssom  16323  ss1oel2o  16380  nninfsellemdc  16406  nninfsellemsuc  16408  nninfsellemqall  16411  trirec0xor  16443  iswomni0  16449