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  684  mt2bi  686  orbi12i  766  or42  774  pm5.53  804  orddi  822  anddi  823  pm2.1dc  839  dcim  843  notnotrdc  845  dcnnOLD  851  rbaib  923  rbaibr  924  pm4.43  952  orbididc  956  pm5.75  965  3orass  984  3anass  985  3ancomb  989  3anan32  992  3anan12  993  anandi3  994  anandi3r  995  xordc  1412  falbitru  1437  19.26-2  1506  19.26-3an  1507  alrot3  1509  albiim  1511  2albiim  1512  19.27h  1584  19.27  1585  19.28h  1586  19.28  1587  nfalt  1602  aaanh  1610  aaan  1611  alinexa  1627  19.21-2  1691  nf2  1692  19.44  1706  19.45  1707  exrot3  1714  exrot4  1715  eeor  1719  sbcof2  1834  sbid2h  1873  19.23vv  1908  sbnv  1913  sblimv  1919  pm11.53  1920  19.41vv  1928  19.41vvv  1929  19.41vvvv  1930  exdistrv  1935  19.42vv  1936  19.42vvv  1937  19.42vvvv  1938  4exdistr  1941  cbvex4v  1959  eean  1960  sbn  1981  sbim  1982  sbor  1983  sban  1984  sbrim  1985  sblim  1986  sbbi  1988  sblbis  1989  sbrbis  1990  sbrbif  1991  sbco2d  1995  sbco2vd  1996  sbnf2  2010  2sb5  2012  2sb6  2013  sbcom2v  2014  sbcom2v2  2015  sbcom2  2016  sb6a  2017  2sb5rf  2018  2sb6rf  2019  sbalyz  2028  sbal  2029  sbal1yz  2030  sbex  2033  sbalv  2034  sbco4lem  2035  exsb  2037  2exsb  2038  eujust  2057  euf  2060  cbveu  2079  mor  2097  eu2  2099  mo4f  2115  eu4  2117  2exeu  2147  2eu4  2148  exists1  2151  abid  2194  eleq12i  2274  abeq2  2315  abeq2i  2317  clabel  2333  abid2f  2375  sbabel  2376  neeq12i  2394  neanior  2464  ralnex  2495  dfrex2dc  2498  ralinexa  2534  nfraldya  2542  nfrexdya  2543  r3al  2551  r19.26-2  2636  ralbiim  2641  ralnex2  2646  r19.43  2665  ralcomf  2668  rexcomf  2669  ralrot3  2672  rexrot4  2674  reean  2676  3reeanv  2678  rabbi  2685  cbvralf  2731  cbvrexf  2732  cbvreu  2737  cbvral2vw  2750  cbvrex2vw  2751  cbvral2v  2752  cbvrex2v  2753  cbvral3v  2754  cbvralsv  2755  cbvrexsv  2756  sbralie  2757  rabeq2i  2770  issetf  2780  2gencl  2806  3gencl  2807  ceqsex2  2814  ceqsex3v  2816  ceqsex6v  2818  ceqsex8v  2819  gencbvex  2820  gencbval  2822  spc2gv  2865  eqvincf  2899  ceqsrex2v  2906  clel5  2911  elrab2  2933  ralab  2934  ralrab  2935  rexab  2936  rexrab  2937  ralab2  2938  rexab2  2940  eueq3dc  2948  morex  2958  euind  2961  reu2  2962  reu6  2963  rmo4  2967  reu4  2968  reu7  2969  rmo3f  2971  rmo4f  2972  rmoim  2975  2reuswapdc  2978  reuind  2979  2rmorex  2980  sbcco  3021  sbccomlem  3074  sbccom  3075  ra5  3088  rmo3  3091  csbco  3104  csbcow  3105  sbnfc2  3155  csbabg  3156  cbvralcsf  3157  cbvrexcsf  3158  cbvreucsf  3159  dfss  3181  dfss2f  3185  ss2ab  3262  dfdif3  3284  difeqri  3294  ddifstab  3306  raldifb  3314  uneqri  3316  ssequn2  3347  unss  3348  rexun  3354  ralunb  3355  elin2  3362  ineqri  3367  dfss1  3378  dfss5  3379  dfss4st  3407  ssddif  3408  difin  3411  indif  3417  difundi  3426  indifdir  3430  symdifxor  3440  inrab2  3447  rabun2  3453  reuun2  3457  0el  3484  rabeq0  3491  abeq0  3492  disjr  3511  disj1  3512  undif4  3524  uneqdifeqim  3547  r19.2m  3548  r19.3rm  3550  r19.9rmv  3553  raaan  3567  pwss  3633  dfpr2  3653  rexdifpr  3662  ralsnsg  3671  ralsns  3672  eltpg  3679  eldiftp  3680  ralprg  3685  rexprg  3686  raltpg  3687  rextpg  3688  snprc  3699  rabrsndc  3702  euabsn2  3703  eusn  3708  eldifsn  3762  ssdifsn  3763  rexdifsn  3767  eqsnm  3798  tpss  3801  snsssn  3804  prel12  3814  preqsn  3818  oprcl  3845  pwtpss  3849  eluniab  3864  elunirab  3865  unipr  3866  dfnfc2  3870  uniun  3871  uniin  3872  uni0b  3877  unissb  3882  elintab  3898  elintrab  3899  ssintab  3904  ssintrab  3910  intun  3918  intpr  3919  elrint  3927  iuncom4  3936  iuneq2  3945  dfiun2g  3961  ssiinf  3979  iundif2ss  3995  elriin  4000  iunxiun  4011  pwssb  4015  elpwpw  4016  iunpwss  4021  dfdisj2  4025  disjiun  4042  cbvopab1  4121  dftr5  4149  trint  4161  inex1  4182  inuni  4203  repizf2lem  4209  unidif0  4215  axpweq  4219  bnd2  4221  exmid01  4246  zfpair2  4258  exss  4275  elop  4279  opm  4282  otth  4290  copsex4g  4295  opeqsn  4301  opelopabsbALT  4309  brabga  4314  opelopabaf  4324  iunopab  4332  pwunss  4334  pocl  4354  frirrg  4401  elsuci  4454  elsucg  4455  sucel  4461  unisucg  4465  uniuni  4502  reusv3  4511  iunpw  4531  setindel  4590  elirr  4593  en2lp  4606  ordpwsucss  4619  zfregfr  4626  tfi  4634  peano2  4647  peano5  4650  elxp  4696  opelxp  4709  brxp  4710  rabxp  4716  opthprc  4730  brab2a  4732  opeliunxp  4734  xpundi  4735  xpundir  4736  elvvv  4742  brinxp  4747  brab2ga  4754  0xp  4759  ssrel2  4769  eqrelrel  4780  reliun  4800  reluni  4802  raliunxp  4823  rexiunxp  4824  ralxpf  4828  rexxpf  4829  iunxpf  4830  relop  4832  elco  4848  elcnv  4859  elcnv2  4860  dmin  4891  dmuni  4893  dmopab  4894  dmi  4898  dmmrnm  4902  rnopab  4930  elrnmpt1  4934  rncoeq  4957  resiexg  5009  restidsing  5020  dfima2  5029  dfima3  5030  elima2  5033  elima3  5034  imai  5043  elimasn  5054  epini  5058  dfse2  5060  cotr  5069  issref  5070  intasym  5072  asymref  5073  cnvopab  5089  cnvi  5092  cnvdif  5094  imainss  5103  rnxpid  5122  dfrel2  5138  dfrel3  5145  dmsnm  5153  rnsnm  5154  relsn2m  5158  dmsnopg  5159  cnvcnvsn  5164  elxp4  5175  elxp5  5176  cnvresima  5177  mptpreima  5181  dfco2  5187  coundi  5189  coundir  5190  imaco  5193  coiun  5197  coi1  5203  relssdmrn  5208  relrelss  5214  unixpm  5223  ressn  5228  cnviinm  5229  cnvpom  5230  cnvsom  5231  cbviota  5242  iotass  5254  eliota  5264  dffun2  5286  dffun4  5287  dffun7  5303  dffun8  5304  dffun9  5305  funopab  5311  funun  5320  funcnvsn  5324  fntpg  5335  funcnv2  5339  funcnv  5340  fun2cnv  5343  fncnv  5345  fun11  5346  fununi  5347  imadiflem  5358  imadif  5359  imainlem  5360  funimaexglem  5362  fnunsn  5388  fnres  5398  fnopabg  5405  mptfng  5407  mptun  5413  fun  5454  fcnvres  5466  dff12  5487  f1cnvcnv  5499  funforn  5512  dff1o2  5534  dff1o5  5538  f1orn  5539  resdif  5551  ffoss  5561  f11o  5562  f1o00  5564  fo00  5565  elfv  5581  fv3  5606  nfvres  5617  eqfnfv3  5686  fneqeql  5695  unpreima  5712  respreima  5715  dffo3  5734  dffo5  5736  f1ompt  5738  ffnfvf  5746  fmptco  5753  funopdmsn  5771  ftpg  5775  fnressn  5777  idref  5832  abrexco  5835  dff13  5844  dff13f  5846  fliftel  5869  isoini  5894  eusvobj2  5937  acexmidlema  5942  acexmidlemb  5943  acexmidlemph  5944  acexmidlem2  5948  oprabid  5983  brabvv  5998  dfoprab2  5999  eqoprab2b  6010  dmoprab  6033  rnoprab  6035  eloprabga  6039  mpomptx  6043  resoprab  6048  ffnov  6056  elrnmpo  6066  ralrnmpo  6067  rexrnmpo  6068  ovid  6069  ovi3  6090  ov6g  6091  foov  6100  opabex3d  6213  opabex3  6214  abexssex  6217  oprabex3  6221  oprabrexex2  6222  fmpo  6294  xporderlem  6324  f1od2  6328  mpoxopovel  6334  brtpos2  6344  dmtpos  6349  tpostpos  6357  tpossym  6369  tposoprab  6373  dfsmo2  6380  tfrlem7  6410  tfrlem9  6412  tfr1onlemaccex  6441  tfrcllemaccex  6454  tfrcldm  6456  frecabex  6491  el1o  6530  dif1o  6531  dfer2  6628  brdifun  6654  eqerlem  6658  qsid  6694  iinerm  6701  riinerm  6702  erinxp  6703  brecop  6719  eroveu  6720  erovlem  6721  ecopovsym  6725  mapval2  6772  mapsn  6784  elixp  6799  ixpeq2  6806  ixpin  6817  ixpiinm  6818  mptelixpg  6828  ixpsnf1o  6830  domen  6847  isfi  6859  en1  6898  xpsnen  6923  xpcomco  6928  xpassen  6932  ssenen  6955  nneneq  6961  snnen2oprc  6964  ac6sfi  7002  exmidpw  7012  exmidpweq  7013  pw1dc1  7018  eldju  7177  djur  7178  eldju2ndl  7181  eldju2ndr  7182  finomni  7249  nninfwlporlemd  7281  nninfwlpoimlemg  7284  acfun  7326  pw1nel3  7350  sucpw1nel3  7352  ccfunen  7383  elni  7428  ltexpi  7457  enq0enq  7551  enq0ref  7553  enq0tr  7554  prarloclem3  7617  ltdfpr  7626  genpdflem  7627  genpassl  7644  genpassu  7645  nqprrnd  7663  nqprl  7671  nqpru  7672  ltexprlemopl  7721  ltexprlemopu  7723  ltexprlemdisj  7726  ltexprlemloc  7727  recexprlemdisj  7750  caucvgprprlemell  7805  caucvgprprlemelu  7806  suplocexprlemml  7836  suplocsrlemb  7926  opelcn  7946  elreal  7948  elreal2  7950  peano1nnnn  7972  axicn  7983  axaddf  7988  axmulf  7989  axprecex  8000  axpre-ltirr  8002  axpre-mulgt0  8007  axcaucvglemres  8019  axpre-suploc  8022  xrlenlt  8144  ltxrlt  8145  inelr  8664  reapcotr  8678  1nn  9054  elnnne0  9316  un0addcl  9335  un0mulcl  9336  elnnz  9389  elznn0nn  9393  elznn0  9394  elznn  9395  elz2  9451  zapne  9454  3halfnz  9477  prime  9479  raluz2  9707  rexuz2  9709  supinfneg  9723  infsupneg  9724  eluz2b2  9731  eluz2b3  9732  ublbneg  9741  elq  9750  qreccl  9770  elpq  9777  ralrp  9804  rexrp  9805  rpnegap  9815  ltxr  9904  xrnemnf  9906  xrltso  9925  icc0r  10055  divelunit  10131  fzprval  10211  fztpval  10212  elfz1b  10219  fz01or  10240  4fvwrd4  10269  fzolb  10283  fzolb2  10284  elfzo3  10293  fzouzsplit  10310  elfzo0z  10315  fzo0m  10322  fzind2  10375  ioo0  10409  ico0  10411  ioc0  10412  uzennn  10588  seq3f1olemp  10667  iswrd  11003  caucvgre  11336  cvg1nlemcau  11339  resqrexlemex  11380  climeu  11651  fsum2dlemstep  11789  expcnv  11859  prodsnf  11947  fprod2dlemstep  11977  divides  12144  m1exp1  12256  divalgb  12280  bitsval2  12299  bitsmod  12311  bitscmp  12313  bezoutlemnewy  12361  bezoutlemmain  12363  bezoutlemex  12366  dfgcd2  12379  nnwosdc  12404  lcmgcdlem  12443  isprm2  12483  isprm3  12484  isprm4  12485  isprm5  12508  sqrt2irr  12528  oddpwdc  12540  pythagtriplem19  12649  pythagtrip  12650  pceu  12662  dvdsprmpweqnn  12703  4sqlem2  12756  4sqlem12  12769  dec5dvds2  12780  ennnfoneleminc  12826  ennnfonelemex  12829  ennnfonelemr  12838  ctiunct  12855  infpn2  12871  xpsfrnel  13220  xpsfrnel2  13222  gsum0g  13272  ismnd  13295  dfgrp2e  13404  dfgrp3me  13476  isnsg2  13583  eqger  13604  isabl2  13674  imasabl  13716  isrhm  13964  isrim  13975  isnzr2  13990  lss1d  14189  istps  14548  istps2  14549  isbasis2g  14561  tgval2  14567  txuni2  14772  tx1cn  14785  tx2cn  14786  uptx  14790  txdis1cn  14794  blres  14950  xmeterval  14951  xmeter  14952  isxms2  14968  isms2  14970  metrest  15022  qtopbasss  15037  dedekindicclemicc  15148  limcdifap  15178  plyrecj  15279  pilem1  15295  sincosq1lem  15341  mpodvdsmulf1o  15506  gausslemma2dlem1a  15579  gausslemma2dlem4  15585  lgsquadlem1  15598  lgsquadlem2  15599  2lgslem1b  15610  2sqlem1  15635  decidr  15806  bdcuni  15886  bdcriota  15893  bdinex1  15909  bj-zfpair2  15920  bj-axun2  15925  bj-ssom  15946  ss1oel2o  16002  nninfsellemdc  16021  nninfsellemsuc  16023  nninfsellemqall  16026  trirec0xor  16058  iswomni0  16064