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  1493  19.26-3an  1494  alrot3  1496  albiim  1498  2albiim  1499  19.27h  1571  19.27  1572  19.28h  1573  19.28  1574  nfalt  1589  aaanh  1597  aaan  1598  alinexa  1614  19.21-2  1678  nf2  1679  19.44  1693  19.45  1694  exrot3  1701  exrot4  1702  eeor  1706  sbcof2  1821  sbid2h  1860  19.23vv  1895  sbnv  1900  sblimv  1906  pm11.53  1907  19.41vv  1915  19.41vvv  1916  19.41vvvv  1917  exdistrv  1922  19.42vv  1923  19.42vvv  1924  19.42vvvv  1925  4exdistr  1928  cbvex4v  1946  eean  1947  sbn  1968  sbim  1969  sbor  1970  sban  1971  sbrim  1972  sblim  1973  sbbi  1975  sblbis  1976  sbrbis  1977  sbrbif  1978  sbco2d  1982  sbco2vd  1983  sbnf2  1997  2sb5  1999  2sb6  2000  sbcom2v  2001  sbcom2v2  2002  sbcom2  2003  sb6a  2004  2sb5rf  2005  2sb6rf  2006  sbalyz  2015  sbal  2016  sbal1yz  2017  sbex  2020  sbalv  2021  sbco4lem  2022  exsb  2024  2exsb  2025  eujust  2044  euf  2047  cbveu  2066  mor  2084  eu2  2086  mo4f  2102  eu4  2104  2exeu  2134  2eu4  2135  exists1  2138  abid  2181  eleq12i  2261  abeq2  2302  abeq2i  2304  clabel  2320  abid2f  2362  sbabel  2363  neeq12i  2381  neanior  2451  ralnex  2482  dfrex2dc  2485  ralinexa  2521  nfraldya  2529  nfrexdya  2530  r3al  2538  r19.26-2  2623  ralbiim  2628  ralnex2  2633  r19.43  2652  ralcomf  2655  rexcomf  2656  ralrot3  2659  rexrot4  2661  reean  2663  3reeanv  2665  rabbi  2672  cbvralf  2718  cbvrexf  2719  cbvreu  2724  cbvral2vw  2737  cbvrex2vw  2738  cbvral2v  2739  cbvrex2v  2740  cbvral3v  2741  cbvralsv  2742  cbvrexsv  2743  sbralie  2744  rabeq2i  2757  issetf  2767  2gencl  2793  3gencl  2794  ceqsex2  2800  ceqsex3v  2802  ceqsex6v  2804  ceqsex8v  2805  gencbvex  2806  gencbval  2808  spc2gv  2851  eqvincf  2885  ceqsrex2v  2892  clel5  2897  elrab2  2919  ralab  2920  ralrab  2921  rexab  2922  rexrab  2923  ralab2  2924  rexab2  2926  eueq3dc  2934  morex  2944  euind  2947  reu2  2948  reu6  2949  rmo4  2953  reu4  2954  reu7  2955  rmo3f  2957  rmo4f  2958  rmoim  2961  2reuswapdc  2964  reuind  2965  2rmorex  2966  sbcco  3007  sbccomlem  3060  sbccom  3061  ra5  3074  rmo3  3077  csbco  3090  csbcow  3091  sbnfc2  3141  csbabg  3142  cbvralcsf  3143  cbvrexcsf  3144  cbvreucsf  3145  dfss  3167  dfss2f  3170  ss2ab  3247  dfdif3  3269  difeqri  3279  ddifstab  3291  raldifb  3299  uneqri  3301  ssequn2  3332  unss  3333  rexun  3339  ralunb  3340  elin2  3347  ineqri  3352  dfss1  3363  dfss5  3364  dfss4st  3392  ssddif  3393  difin  3396  indif  3402  difundi  3411  indifdir  3415  symdifxor  3425  inrab2  3432  rabun2  3438  reuun2  3442  0el  3469  rabeq0  3476  abeq0  3477  disjr  3496  disj1  3497  undif4  3509  uneqdifeqim  3532  r19.2m  3533  r19.3rm  3535  r19.9rmv  3538  raaan  3552  pwss  3617  dfpr2  3637  rexdifpr  3646  ralsnsg  3655  ralsns  3656  eltpg  3663  eldiftp  3664  ralprg  3669  rexprg  3670  raltpg  3671  rextpg  3672  snprc  3683  rabrsndc  3686  euabsn2  3687  eusn  3692  eldifsn  3745  ssdifsn  3746  rexdifsn  3750  eqsnm  3781  tpss  3784  snsssn  3787  prel12  3797  preqsn  3801  oprcl  3828  pwtpss  3832  eluniab  3847  elunirab  3848  unipr  3849  dfnfc2  3853  uniun  3854  uniin  3855  uni0b  3860  unissb  3865  elintab  3881  elintrab  3882  ssintab  3887  ssintrab  3893  intun  3901  intpr  3902  elrint  3910  iuncom4  3919  iuneq2  3928  dfiun2g  3944  ssiinf  3962  iundif2ss  3978  elriin  3983  iunxiun  3994  pwssb  3998  elpwpw  3999  iunpwss  4004  dfdisj2  4008  disjiun  4024  cbvopab1  4102  dftr5  4130  trint  4142  inex1  4163  inuni  4184  repizf2lem  4190  unidif0  4196  axpweq  4200  bnd2  4202  exmid01  4227  zfpair2  4239  exss  4256  elop  4260  opm  4263  otth  4271  copsex4g  4276  opeqsn  4281  opelopabsbALT  4289  brabga  4294  opelopabaf  4304  iunopab  4312  pwunss  4314  pocl  4334  frirrg  4381  elsuci  4434  elsucg  4435  sucel  4441  unisucg  4445  uniuni  4482  reusv3  4491  iunpw  4511  setindel  4570  elirr  4573  en2lp  4586  ordpwsucss  4599  zfregfr  4606  tfi  4614  peano2  4627  peano5  4630  elxp  4676  opelxp  4689  brxp  4690  rabxp  4696  opthprc  4710  brab2a  4712  opeliunxp  4714  xpundi  4715  xpundir  4716  elvvv  4722  brinxp  4727  brab2ga  4734  0xp  4739  ssrel2  4749  eqrelrel  4760  reliun  4780  reluni  4782  raliunxp  4803  rexiunxp  4804  ralxpf  4808  rexxpf  4809  iunxpf  4810  relop  4812  elco  4828  elcnv  4839  elcnv2  4840  dmin  4870  dmuni  4872  dmopab  4873  dmi  4877  dmmrnm  4881  rnopab  4909  elrnmpt1  4913  rncoeq  4935  resiexg  4987  restidsing  4998  dfima2  5007  dfima3  5008  elima2  5011  elima3  5012  imai  5021  elimasn  5032  epini  5036  dfse2  5038  cotr  5047  issref  5048  intasym  5050  asymref  5051  cnvopab  5067  cnvi  5070  cnvdif  5072  imainss  5081  rnxpid  5100  dfrel2  5116  dfrel3  5123  dmsnm  5131  rnsnm  5132  relsn2m  5136  dmsnopg  5137  cnvcnvsn  5142  elxp4  5153  elxp5  5154  cnvresima  5155  mptpreima  5159  dfco2  5165  coundi  5167  coundir  5168  imaco  5171  coiun  5175  coi1  5181  relssdmrn  5186  relrelss  5192  unixpm  5201  ressn  5206  cnviinm  5207  cnvpom  5208  cnvsom  5209  cbviota  5220  iotass  5232  eliota  5242  dffun2  5264  dffun4  5265  dffun7  5281  dffun8  5282  dffun9  5283  funopab  5289  funun  5298  funcnvsn  5299  fntpg  5310  funcnv2  5314  funcnv  5315  fun2cnv  5318  fncnv  5320  fun11  5321  fununi  5322  imadiflem  5333  imadif  5334  imainlem  5335  funimaexglem  5337  fnunsn  5361  fnres  5370  fnopabg  5377  mptfng  5379  mptun  5385  fun  5426  fcnvres  5437  dff12  5458  f1cnvcnv  5470  funforn  5483  dff1o2  5505  dff1o5  5509  f1orn  5510  resdif  5522  ffoss  5532  f11o  5533  f1o00  5535  fo00  5536  elfv  5552  fv3  5577  nfvres  5588  eqfnfv3  5657  fneqeql  5666  unpreima  5683  respreima  5686  dffo3  5705  dffo5  5707  f1ompt  5709  ffnfvf  5717  fmptco  5724  ftpg  5742  fnressn  5744  idref  5799  abrexco  5802  dff13  5811  dff13f  5813  fliftel  5836  isoini  5861  eusvobj2  5904  acexmidlema  5909  acexmidlemb  5910  acexmidlemph  5911  acexmidlem2  5915  oprabid  5950  brabvv  5964  dfoprab2  5965  eqoprab2b  5976  dmoprab  5999  rnoprab  6001  eloprabga  6005  mpomptx  6009  resoprab  6014  ffnov  6022  elrnmpo  6032  ralrnmpo  6033  rexrnmpo  6034  ovid  6035  ovi3  6055  ov6g  6056  foov  6065  opabex3d  6173  opabex3  6174  abexssex  6177  oprabex3  6181  oprabrexex2  6182  fmpo  6254  xporderlem  6284  f1od2  6288  mpoxopovel  6294  brtpos2  6304  dmtpos  6309  tpostpos  6317  tpossym  6329  tposoprab  6333  dfsmo2  6340  tfrlem7  6370  tfrlem9  6372  tfr1onlemaccex  6401  tfrcllemaccex  6414  tfrcldm  6416  frecabex  6451  el1o  6490  dif1o  6491  dfer2  6588  brdifun  6614  eqerlem  6618  qsid  6654  iinerm  6661  riinerm  6662  erinxp  6663  brecop  6679  eroveu  6680  erovlem  6681  ecopovsym  6685  mapval2  6732  mapsn  6744  elixp  6759  ixpeq2  6766  ixpin  6777  ixpiinm  6778  mptelixpg  6788  ixpsnf1o  6790  domen  6805  isfi  6815  en1  6853  xpsnen  6875  xpcomco  6880  xpassen  6884  ssenen  6907  nneneq  6913  snnen2oprc  6916  ac6sfi  6954  exmidpw  6964  exmidpweq  6965  pw1dc1  6970  eldju  7127  djur  7128  eldju2ndl  7131  eldju2ndr  7132  finomni  7199  nninfwlporlemd  7231  nninfwlpoimlemg  7234  acfun  7267  pw1nel3  7291  sucpw1nel3  7293  ccfunen  7324  elni  7368  ltexpi  7397  enq0enq  7491  enq0ref  7493  enq0tr  7494  prarloclem3  7557  ltdfpr  7566  genpdflem  7567  genpassl  7584  genpassu  7585  nqprrnd  7603  nqprl  7611  nqpru  7612  ltexprlemopl  7661  ltexprlemopu  7663  ltexprlemdisj  7666  ltexprlemloc  7667  recexprlemdisj  7690  caucvgprprlemell  7745  caucvgprprlemelu  7746  suplocexprlemml  7776  suplocsrlemb  7866  opelcn  7886  elreal  7888  elreal2  7890  peano1nnnn  7912  axicn  7923  axaddf  7928  axmulf  7929  axprecex  7940  axpre-ltirr  7942  axpre-mulgt0  7947  axcaucvglemres  7959  axpre-suploc  7962  xrlenlt  8084  ltxrlt  8085  inelr  8603  reapcotr  8617  1nn  8993  elnnne0  9254  un0addcl  9273  un0mulcl  9274  elnnz  9327  elznn0nn  9331  elznn0  9332  elznn  9333  elz2  9388  zapne  9391  3halfnz  9414  prime  9416  raluz2  9644  rexuz2  9646  supinfneg  9660  infsupneg  9661  eluz2b2  9668  eluz2b3  9669  ublbneg  9678  elq  9687  qreccl  9707  elpq  9714  ralrp  9741  rexrp  9742  rpnegap  9752  ltxr  9841  xrnemnf  9843  xrltso  9862  icc0r  9992  divelunit  10068  fzprval  10148  fztpval  10149  elfz1b  10156  fz01or  10177  4fvwrd4  10206  fzolb  10220  fzolb2  10221  elfzo3  10230  fzouzsplit  10246  elfzo0z  10251  fzo0m  10258  fzind2  10306  ioo0  10328  ico0  10330  ioc0  10331  uzennn  10507  seq3f1olemp  10586  iswrd  10916  caucvgre  11125  cvg1nlemcau  11128  resqrexlemex  11169  climeu  11439  fsum2dlemstep  11577  expcnv  11647  prodsnf  11735  fprod2dlemstep  11765  divides  11932  m1exp1  12042  divalgb  12066  bezoutlemnewy  12133  bezoutlemmain  12135  bezoutlemex  12138  dfgcd2  12151  nnwosdc  12176  lcmgcdlem  12215  isprm2  12255  isprm3  12256  isprm4  12257  isprm5  12280  sqrt2irr  12300  oddpwdc  12312  pythagtriplem19  12420  pythagtrip  12421  pceu  12433  dvdsprmpweqnn  12474  4sqlem2  12527  4sqlem12  12540  ennnfoneleminc  12568  ennnfonelemex  12571  ennnfonelemr  12580  ctiunct  12597  infpn2  12613  xpsfrnel  12927  xpsfrnel2  12929  gsum0g  12979  ismnd  13000  dfgrp2e  13100  dfgrp3me  13172  isnsg2  13273  eqger  13294  isabl2  13364  imasabl  13406  isrhm  13654  isrim  13665  isnzr2  13680  lss1d  13879  istps  14200  istps2  14201  isbasis2g  14213  tgval2  14219  txuni2  14424  tx1cn  14437  tx2cn  14438  uptx  14442  txdis1cn  14446  blres  14602  xmeterval  14603  xmeter  14604  isxms2  14620  isms2  14622  metrest  14674  qtopbasss  14689  dedekindicclemicc  14786  limcdifap  14816  pilem1  14914  sincosq1lem  14960  gausslemma2dlem1a  15174  gausslemma2dlem4  15180  lgsquadlem1  15191  2sqlem1  15201  decidr  15288  bdcuni  15368  bdcriota  15375  bdinex1  15391  bj-zfpair2  15402  bj-axun2  15407  bj-ssom  15428  ss1oel2o  15484  nninfsellemdc  15500  nninfsellemsuc  15502  nninfsellemqall  15505  trirec0xor  15535  iswomni0  15541