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  589  xchbinx  688  mt2bi  690  orbi12i  771  or42  779  pm5.53  809  orddi  827  anddi  828  pm2.1dc  844  dcim  848  notnotrdc  850  dcnnOLD  856  rbaib  928  rbaibr  929  pm4.43  957  orbididc  961  pm5.75  970  ifptru  997  ifpfal  998  3orass  1007  3anass  1008  3ancomb  1012  3anan32  1015  3anan12  1016  anandi3  1017  anandi3r  1018  xordc  1436  falbitru  1461  19.26-2  1530  19.26-3an  1531  alrot3  1533  albiim  1535  2albiim  1536  19.27h  1608  19.27  1609  19.28h  1610  19.28  1611  nfalt  1626  aaanh  1634  aaan  1635  alinexa  1651  19.21-2  1715  nf2  1716  19.44  1730  19.45  1731  exrot3  1738  exrot4  1739  eeor  1743  sbcof2  1858  sbid2h  1897  19.23vv  1932  sbnv  1937  sblimv  1943  pm11.53  1944  19.41vv  1952  19.41vvv  1953  19.41vvvv  1954  exdistrv  1959  19.42vv  1960  19.42vvv  1961  19.42vvvv  1962  4exdistr  1965  cbvex4v  1983  eean  1984  sbn  2005  sbim  2006  sbor  2007  sban  2008  sbrim  2009  sblim  2010  sbbi  2012  sblbis  2013  sbrbis  2014  sbrbif  2015  sbco2d  2019  sbco2vd  2020  sbnf2  2034  2sb5  2036  2sb6  2037  sbcom2v  2038  sbcom2v2  2039  sbcom2  2040  sb6a  2041  2sb5rf  2042  2sb6rf  2043  sbalyz  2052  sbal  2053  sbal1yz  2054  sbex  2057  sbalv  2058  sbco4lem  2059  exsb  2061  2exsb  2062  eujust  2081  euf  2084  cbveu  2103  mor  2122  eu2  2124  mo4f  2140  eu4  2142  2exeu  2172  2eu4  2173  exists1  2176  abid  2219  eleq12i  2299  abeq2  2340  abeq2i  2342  clabel  2358  abid2f  2400  sbabel  2401  neeq12i  2419  neanior  2489  ralnex  2520  dfrex2dc  2523  ralinexa  2559  nfraldya  2567  nfrexdya  2568  r3al  2576  r19.26-2  2662  ralbiim  2667  ralnex2  2672  r19.43  2691  ralcomf  2694  rexcomf  2695  ralrot3  2698  rexrot4  2700  reean  2702  3reeanv  2704  rabbi  2711  cbvralf  2758  cbvrexf  2759  cbvreu  2765  cbvral2vw  2778  cbvrex2vw  2779  cbvral2v  2780  cbvrex2v  2781  cbvral3v  2782  cbvralsv  2783  cbvrexsv  2784  sbralie  2785  rabeq2i  2799  issetf  2810  2gencl  2836  3gencl  2837  ceqsex2  2844  ceqsex3v  2846  ceqsex6v  2848  ceqsex8v  2849  gencbvex  2850  gencbval  2852  spc2gv  2897  eqvincf  2931  ceqsrex2v  2938  clel5  2943  elrab2  2965  ralab  2966  ralrab  2967  rexab  2968  rexrab  2969  ralab2  2970  rexab2  2972  eueq3dc  2980  morex  2990  euind  2993  reu2  2994  reu6  2995  rmo4  2999  reu4  3000  reu7  3001  rmo3f  3003  rmo4f  3004  rmoim  3007  2reuswapdc  3010  reuind  3011  2rmorex  3012  sbcco  3053  sbccomlem  3106  sbccom  3107  ra5  3121  rmo3  3124  csbco  3137  csbcow  3138  sbnfc2  3188  csbabg  3189  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  dfss  3214  dfss2f  3218  ss2ab  3295  dfdif3  3317  difeqri  3327  ddifstab  3339  raldifb  3347  uneqri  3349  ssequn2  3380  unss  3381  rexun  3387  ralunb  3388  elin2  3395  ineqri  3400  dfss1  3411  dfss5  3412  dfss4st  3440  ssddif  3441  difin  3444  indif  3450  difundi  3459  indifdir  3463  symdifxor  3473  inrab2  3480  rabun2  3486  reuun2  3490  0el  3517  rabeq0  3524  abeq0  3525  disjr  3544  disj1  3545  undif4  3557  uneqdifeqim  3580  r19.2m  3581  r19.3rm  3583  r19.9rmv  3586  raaan  3600  pwss  3668  dfpr2  3688  rexdifpr  3697  ralsnsg  3706  ralsns  3707  eltpg  3714  eldiftp  3715  ralprg  3720  rexprg  3721  raltpg  3722  rextpg  3723  snprc  3734  rabrsndc  3739  euabsn2  3740  eusn  3745  eldifsn  3800  ssdifsn  3801  rexdifsn  3805  eqsnm  3838  tpss  3841  snsssn  3844  prel12  3854  preqsn  3858  oprcl  3886  pwtpss  3890  eluniab  3905  elunirab  3906  unipr  3907  dfnfc2  3911  uniun  3912  uniin  3913  uni0b  3918  unissb  3923  elintab  3939  elintrab  3940  ssintab  3945  ssintrab  3951  intun  3959  intpr  3960  elrint  3968  iuncom4  3977  iuneq2  3986  dfiun2g  4002  ssiinf  4020  iundif2ss  4036  elriin  4041  iunxiun  4052  pwssb  4056  elpwpw  4057  iunpwss  4062  dfdisj2  4066  disjiun  4083  cbvopab1  4162  dftr5  4190  trint  4202  inex1  4223  inuni  4245  repizf2lem  4251  unidif0  4257  axpweq  4261  bnd2  4263  exmid01  4288  zfpair2  4300  exss  4319  elop  4323  opm  4326  otth  4334  copsex4g  4339  opeqsn  4345  opelopabsbALT  4353  brabga  4358  opelopabaf  4368  iunopab  4376  pwunss  4380  pocl  4400  frirrg  4447  elsuci  4500  elsucg  4501  sucel  4507  unisucg  4511  uniuni  4548  reusv3  4557  iunpw  4577  setindel  4636  elirr  4639  en2lp  4652  ordpwsucss  4665  zfregfr  4672  tfi  4680  peano2  4693  peano5  4696  elxp  4742  opelxp  4755  brxp  4756  rabxp  4763  opthprc  4777  brab2a  4779  opeliunxp  4781  xpundi  4782  xpundir  4783  elvvv  4789  brinxp  4794  brab2ga  4801  0xp  4806  ssrel2  4816  eqrelrel  4827  reliun  4848  reluni  4850  raliunxp  4871  rexiunxp  4872  ralxpf  4876  rexxpf  4877  iunxpf  4878  relop  4880  elco  4896  elcnv  4907  elcnv2  4908  dmin  4939  dmuni  4941  dmopab  4942  dmi  4946  dmmrnm  4951  rnopab  4979  elrnmpt1  4983  rncoeq  5006  resiexg  5058  restidsing  5069  dfima2  5078  dfima3  5079  elima2  5082  elima3  5083  imai  5092  elimasn  5103  epini  5107  dfse2  5109  cotr  5118  issref  5119  intasym  5121  asymref  5122  cnvopab  5138  cnvi  5141  cnvdif  5143  imainss  5152  rnxpid  5171  dfrel2  5187  dfrel3  5194  dmsnm  5202  rnsnm  5203  relsn2m  5207  dmsnopg  5208  cnvcnvsn  5213  elxp4  5224  elxp5  5225  cnvresima  5226  mptpreima  5230  dfco2  5236  coundi  5238  coundir  5239  imaco  5242  coiun  5246  coi1  5252  relssdmrn  5257  relrelss  5263  unixpm  5272  ressn  5277  cnviinm  5278  cnvpom  5279  cnvsom  5280  cbviota  5291  iotass  5304  eliota  5314  dffun2  5336  dffun4  5337  dffun7  5353  dffun8  5354  dffun9  5355  funopab  5361  funun  5371  funcnvsn  5375  fntpg  5386  funcnv2  5390  funcnv  5391  fun2cnv  5394  fncnv  5396  fun11  5397  fununi  5398  imadiflem  5409  imadif  5410  imainlem  5411  funimaexglem  5413  fnunsn  5439  fnres  5449  fnopabg  5456  mptfng  5458  mptun  5464  fun  5508  fcnvres  5520  dff12  5541  f1cnvcnv  5553  funforn  5566  dff1o2  5588  dff1o5  5592  f1orn  5593  resdif  5605  ffoss  5616  f11o  5617  f1o00  5620  fo00  5621  elfv  5637  fv3  5662  nfvres  5675  eqfnfv3  5746  fneqeql  5755  unpreima  5772  respreima  5775  dffo3  5794  dffo5  5796  f1ompt  5798  ffnfvf  5806  fmptco  5813  funopdmsn  5834  ftpg  5838  fnressn  5840  idref  5897  abrexco  5900  dff13  5909  dff13f  5911  fliftel  5934  isoini  5959  eusvobj2  6004  acexmidlema  6009  acexmidlemb  6010  acexmidlemph  6011  acexmidlem2  6015  oprabid  6050  brabvv  6067  dfoprab2  6068  eqoprab2b  6079  dmoprab  6102  rnoprab  6104  eloprabga  6108  mpomptx  6112  resoprab  6117  ffnov  6125  elrnmpo  6135  ralrnmpo  6136  rexrnmpo  6137  ovid  6138  ovi3  6159  ov6g  6160  foov  6169  opabex3d  6283  opabex3  6284  abexssex  6287  oprabex3  6291  oprabrexex2  6292  fmpo  6366  xporderlem  6396  f1od2  6400  mpoxopovel  6407  brtpos2  6417  dmtpos  6422  tpostpos  6430  tpossym  6442  tposoprab  6446  dfsmo2  6453  tfrlem7  6483  tfrlem9  6485  tfr1onlemaccex  6514  tfrcllemaccex  6527  tfrcldm  6529  frecabex  6564  el1o  6605  dif1o  6606  dfer2  6703  brdifun  6729  eqerlem  6733  qsid  6769  iinerm  6776  riinerm  6777  erinxp  6778  brecop  6794  eroveu  6795  erovlem  6796  ecopovsym  6800  mapval2  6847  mapsn  6859  elixp  6874  ixpeq2  6881  ixpin  6892  ixpiinm  6893  mptelixpg  6903  ixpsnf1o  6905  domen  6922  isfi  6934  en1  6973  modom2  6995  xpsnen  7005  xpcomco  7010  xpassen  7014  ssenen  7037  nneneq  7043  snnen2oprc  7046  ac6sfi  7087  exmidpw  7100  exmidpweq  7101  pw1dc1  7106  eldju  7267  djur  7268  eldju2ndl  7271  eldju2ndr  7272  finomni  7339  nninfwlporlemd  7371  nninfwlpoimlemg  7374  acfun  7422  pw1nel3  7449  sucpw1nel3  7451  ccfunen  7483  elni  7528  ltexpi  7557  enq0enq  7651  enq0ref  7653  enq0tr  7654  prarloclem3  7717  ltdfpr  7726  genpdflem  7727  genpassl  7744  genpassu  7745  nqprrnd  7763  nqprl  7771  nqpru  7772  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemdisj  7826  ltexprlemloc  7827  recexprlemdisj  7850  caucvgprprlemell  7905  caucvgprprlemelu  7906  suplocexprlemml  7936  suplocsrlemb  8026  opelcn  8046  elreal  8048  elreal2  8050  peano1nnnn  8072  axicn  8083  axaddf  8088  axmulf  8089  axprecex  8100  axpre-ltirr  8102  axpre-mulgt0  8107  axcaucvglemres  8119  axpre-suploc  8122  xrlenlt  8244  ltxrlt  8245  inelr  8764  reapcotr  8778  1nn  9154  elnnne0  9416  un0addcl  9435  un0mulcl  9436  elnnz  9489  elznn0nn  9493  elznn0  9494  elznn  9495  elz2  9551  zapne  9554  3halfnz  9577  prime  9579  raluz2  9813  rexuz2  9815  supinfneg  9829  infsupneg  9830  eluz2b2  9837  eluz2b3  9838  ublbneg  9847  elq  9856  qreccl  9876  elpq  9883  ralrp  9910  rexrp  9911  rpnegap  9921  ltxr  10010  xrnemnf  10012  xrltso  10031  icc0r  10161  divelunit  10237  fzprval  10317  fztpval  10318  elfz1b  10325  fz01or  10346  4fvwrd4  10375  fzolb  10389  fzolb2  10390  elfzo3  10399  fzouzsplit  10416  elfzo0z  10424  fzo0m  10432  fzind2  10486  ioo0  10520  ico0  10522  ioc0  10523  uzennn  10699  seq3f1olemp  10778  iswrd  11116  caucvgre  11543  cvg1nlemcau  11546  resqrexlemex  11587  climeu  11858  fsum2dlemstep  11997  expcnv  12067  prodsnf  12155  fprod2dlemstep  12185  divides  12352  m1exp1  12464  divalgb  12488  bitsval2  12507  bitsmod  12519  bitscmp  12521  bezoutlemnewy  12569  bezoutlemmain  12571  bezoutlemex  12574  dfgcd2  12587  nnwosdc  12612  lcmgcdlem  12651  isprm2  12691  isprm3  12692  isprm4  12693  isprm5  12716  sqrt2irr  12736  oddpwdc  12748  pythagtriplem19  12857  pythagtrip  12858  pceu  12870  dvdsprmpweqnn  12911  4sqlem2  12964  4sqlem12  12977  dec5dvds2  12988  ennnfoneleminc  13034  ennnfonelemex  13037  ennnfonelemr  13046  ctiunct  13063  infpn2  13079  xpsfrnel  13429  xpsfrnel2  13431  gsum0g  13481  ismnd  13504  dfgrp2e  13613  dfgrp3me  13685  isnsg2  13792  eqger  13813  isabl2  13883  imasabl  13925  isrhm  14175  isrim  14186  isnzr2  14201  lss1d  14400  istps  14759  istps2  14760  isbasis2g  14772  tgval2  14778  txuni2  14983  tx1cn  14996  tx2cn  14997  uptx  15001  txdis1cn  15005  blres  15161  xmeterval  15162  xmeter  15163  isxms2  15179  isms2  15181  metrest  15233  qtopbasss  15248  dedekindicclemicc  15359  limcdifap  15389  plyrecj  15490  pilem1  15506  sincosq1lem  15552  mpodvdsmulf1o  15717  gausslemma2dlem1a  15790  gausslemma2dlem4  15796  lgsquadlem1  15809  lgsquadlem2  15810  2lgslem1b  15821  2sqlem1  15846  upgrex  15957  griedg0ssusgr  16105  clwwlkn1loopb  16274  clwwlknon2x  16289  decidr  16413  bdcuni  16492  bdcriota  16499  bdinex1  16515  bj-zfpair2  16526  bj-axun2  16531  bj-ssom  16552  ss1oel2o  16607  nninfsellemdc  16633  nninfsellemsuc  16635  nninfsellemqall  16638  trirec0xor  16670  iswomni0  16676