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  689  mt2bi  691  orbi12i  772  or42  780  pm5.53  810  orddi  828  anddi  829  pm2.1dc  845  dcim  849  notnotrdc  851  dcnnOLD  857  rbaib  929  rbaibr  930  pm4.43  958  orbididc  962  pm5.75  971  ifptru  998  ifpfal  999  3orass  1008  3anass  1009  3ancomb  1013  3anan32  1016  3anan12  1017  anandi3  1018  anandi3r  1019  xordc  1437  falbitru  1462  19.26-2  1531  19.26-3an  1532  alrot3  1534  albiim  1536  2albiim  1537  19.27h  1609  19.27  1610  19.28h  1611  19.28  1612  nfalt  1627  aaanh  1635  aaan  1636  alinexa  1652  19.21-2  1715  nf2  1716  19.44  1730  19.45  1731  exrot3  1738  exrot4  1739  eeor  1743  sbcof2  1859  sbid2h  1898  19.23vv  1933  sbnv  1938  sblimv  1944  pm11.53  1945  19.41vv  1953  19.41vvv  1954  19.41vvvv  1955  exdistrv  1960  19.42vv  1961  19.42vvv  1962  19.42vvvv  1963  4exdistr  1966  cbvex4v  1984  eean  1985  sbn  2006  sbim  2007  sbor  2008  sban  2009  sbrim  2010  sblim  2011  sbbi  2013  sblbis  2014  sbrbis  2015  sbrbif  2016  sbco2d  2020  sbco2vd  2021  sbnf2  2035  2sb5  2037  2sb6  2038  sbcom2v  2039  sbcom2v2  2040  sbcom2  2041  sb6a  2042  2sb5rf  2043  2sb6rf  2044  sbalyz  2053  sbal  2054  sbal1yz  2055  sbex  2058  sbalv  2059  sbco4lem  2060  exsb  2062  2exsb  2063  eujust  2082  euf  2085  cbveu  2104  mor  2123  eu2  2125  mo4f  2141  eu4  2143  2exeu  2173  2eu4  2174  exists1  2177  abid  2220  eleq12i  2300  abeq2  2341  abeq2i  2343  abbib  2350  clabel  2361  eqabb  2368  abid2f  2410  sbabel  2411  neeq12i  2429  neanior  2499  ralnex  2530  dfrex2dc  2533  ralinexa  2569  nfraldya  2577  nfrexdya  2578  r3al  2586  r19.26-2  2672  ralbiim  2677  ralnex2  2682  r19.43  2701  ralcomf  2704  rexcomf  2705  ralrot3  2708  rexrot4  2710  reean  2712  3reeanv  2714  rabbi  2721  cbvralf  2768  cbvrexf  2769  cbvreu  2775  cbvral2vw  2788  cbvrex2vw  2789  cbvral2v  2790  cbvrex2v  2791  cbvral3v  2792  cbvralsv  2793  cbvrexsv  2794  sbralie  2795  rabeq2i  2809  issetf  2820  2gencl  2846  3gencl  2847  ceqsex2  2854  ceqsex3v  2856  ceqsex6v  2858  ceqsex8v  2859  gencbvex  2860  gencbval  2862  spc2gv  2907  eqvincf  2941  ceqsrex2v  2948  clel5  2953  elrab2  2975  ralab  2976  ralrab  2977  rexab  2978  rexrab  2979  ralab2  2980  rexab2  2982  eueq3dc  2990  morex  3000  euind  3003  reu2  3004  reu6  3005  rmo4  3009  reu4  3010  reu7  3011  rmo3f  3013  rmo4f  3014  rmoim  3017  2reuswapdc  3020  reuind  3021  2rmorex  3022  sbcco  3063  sbccomlem  3116  sbccom  3117  ra5  3131  rmo3  3134  csbco  3147  csbcow  3148  sbnfc2  3198  csbabg  3199  cbvralcsf  3200  cbvrexcsf  3201  cbvreucsf  3202  dfss  3224  dfss2f  3228  ss2ab  3305  dfdif3  3328  difeqri  3338  ddifstab  3350  raldifb  3358  uneqri  3360  ssequn2  3391  unss  3392  rexun  3398  ralunb  3399  elin2  3406  ineqri  3413  dfss1  3424  dfss5  3425  dfss4st  3453  ssddif  3454  difin  3457  indif  3463  difundi  3472  indifdir  3476  symdifxor  3486  inrab2  3493  rabun2  3499  reuun2  3503  0el  3530  rabeq0  3537  abeq0  3538  disjr  3557  disj1  3558  undif4  3570  uneqdifeqim  3594  r19.2m  3595  r19.3rm  3597  r19.9rmv  3600  raaan  3614  pwss  3687  dfpr2  3707  rexdifpr  3716  ralsnsg  3725  ralsns  3726  eltpg  3733  eldiftp  3734  ralprg  3739  rexprg  3740  raltpg  3741  rextpg  3742  snprc  3753  rabrsndc  3758  euabsn2  3759  eusn  3764  eldifsn  3819  ssdifsn  3820  rexdifsn  3824  eqsnm  3858  tpss  3861  snsssn  3864  prel12  3874  preqsn  3878  oprcl  3906  pwtpss  3910  eluniab  3925  elunirab  3926  unipr  3927  dfnfc2  3931  uniun  3932  uniin  3933  uni0b  3938  unissb  3943  elintab  3959  elintrab  3960  ssintab  3965  ssintrab  3971  intun  3979  intpr  3980  elrint  3988  iuncom4  3997  iuneq2  4006  dfiun2g  4022  ssiinf  4040  iundif2ss  4056  elriin  4061  iunxiun  4072  pwssb  4076  elpwpw  4077  iunpwss  4082  dfdisj2  4086  disjiun  4103  cbvopab1  4182  dftr5  4210  trint  4222  inex1  4243  inuni  4266  repizf2lem  4273  unidif0  4279  axpweq  4283  bnd2  4285  exmid01  4310  zfpair2  4322  exss  4342  elop  4346  opm  4349  otth  4357  copsex4g  4362  opeqsn  4368  opelopabsbALT  4376  brabga  4381  opelopabaf  4391  iunopab  4399  pwunss  4403  pocl  4423  frirrg  4470  elsuci  4523  elsucg  4524  sucel  4530  unisucg  4534  uniuni  4571  reusv3  4580  iunpw  4600  setindel  4659  elirr  4662  en2lp  4675  ordpwsucss  4688  zfregfr  4695  tfi  4703  peano2  4716  peano5  4719  elxp  4765  opelxp  4778  brxp  4779  rabxp  4786  opthprc  4800  brab2a  4802  opeliunxp  4804  xpundi  4805  xpundir  4806  elvvv  4812  brinxp  4817  brab2ga  4824  0xp  4829  ssrel2  4839  eqrelrel  4850  reliun  4872  reluni  4874  raliunxp  4895  rexiunxp  4896  ralxpf  4900  rexxpf  4901  iunxpf  4902  relop  4904  elco  4920  elcnv  4931  elcnv2  4932  dmin  4963  dmuni  4965  dmopab  4966  dmi  4970  dmmrnm  4975  rnopab  5003  elrnmpt1  5007  rncoeq  5030  resiexg  5082  restidsing  5093  dfima2  5102  dfima3  5103  elima2  5106  elima3  5107  imai  5117  elimasn  5128  epini  5132  dfse2  5134  cotr  5143  issref  5144  intasym  5146  asymref  5147  cnvopab  5163  cnvi  5166  cnvdif  5168  imainss  5177  rnxpid  5196  dfrel2  5212  dfrel3  5219  dmsnm  5227  rnsnm  5228  relsn2m  5232  dmsnopg  5233  cnvcnvsn  5238  elxp4  5249  elxp5  5250  cnvresima  5251  mptpreima  5255  dfco2  5261  coundi  5263  coundir  5264  imaco  5267  coiun  5271  coi1  5277  relssdmrn  5282  relrelss  5288  unixpm  5297  ressn  5302  cnviinm  5303  cnvpom  5304  cnvsom  5305  cbviota  5316  iotass  5329  eliota  5339  dffun2  5361  dffun4  5362  dffun7  5378  dffun8  5379  dffun9  5380  funopab  5386  funun  5396  funcnvsn  5400  fntpg  5411  funcnv2  5415  funcnv  5416  fun2cnv  5419  fncnv  5421  fun11  5422  fununi  5423  imadiflem  5434  imadif  5435  imainlem  5436  funimaexglem  5438  fnunsn  5464  fnres  5474  fnopabg  5481  mptfng  5483  mptun  5489  fun  5535  fcnvres  5549  dff12  5571  f1cnvcnv  5583  funforn  5596  dff1o2  5618  dff1o5  5622  f1orn  5623  resdif  5635  ffoss  5646  f11o  5647  f1o00  5650  fo00  5651  elfv  5667  fv3  5692  nfvres  5705  eqfnfv3  5776  fneqeql  5785  unpreima  5801  respreima  5804  dffo3  5823  dffo5  5825  f1ompt  5827  ffnfvf  5835  fmptco  5842  funopdmsn  5863  ftpg  5867  fnressn  5869  idref  5928  abrexco  5931  dff13  5940  dff13f  5942  fliftel  5965  isoini  5990  eusvobj2  6035  acexmidlema  6040  acexmidlemb  6041  acexmidlemph  6042  acexmidlem2  6046  oprabid  6081  brabvv  6098  dfoprab2  6099  eqoprab2b  6110  dmoprab  6133  rnoprab  6135  eloprabga  6139  mpomptx  6143  resoprab  6148  ffnov  6156  elrnmpo  6166  ralrnmpo  6167  rexrnmpo  6168  ovid  6169  ovi3  6190  ov6g  6191  foov  6200  opabex3d  6313  opabex3  6314  abexssex  6317  oprabex3  6321  oprabrexex2  6322  fmpo  6396  xporderlem  6426  f1od2  6430  mpoxopovel  6471  brtpos2  6481  dmtpos  6486  tpostpos  6494  tpossym  6506  tposoprab  6510  dfsmo2  6517  tfrlem7  6547  tfrlem9  6549  tfr1onlemaccex  6578  tfrcllemaccex  6591  tfrcldm  6593  frecabex  6628  el1o  6669  dif1o  6670  dfer2  6767  brdifun  6793  eqerlem  6797  qsid  6833  iinerm  6840  riinerm  6841  erinxp  6842  brecop  6858  eroveu  6859  erovlem  6860  ecopovsym  6864  mapval2  6911  mapsn  6924  elixp  6939  ixpeq2  6946  ixpin  6957  ixpiinm  6958  mptelixpg  6968  ixpsnf1o  6970  domen  6987  isfi  6999  en1  7038  modom2  7061  xpsnen  7071  xpcomco  7076  xpassen  7080  ssenen  7104  nneneq  7110  snnen2oprc  7113  ac6sfi  7154  exmidpw  7167  exmidpweq  7168  pw1dc1  7173  elfpw  7214  eldju  7358  djur  7359  eldju2ndl  7362  eldju2ndr  7363  finomni  7430  nninfwlporlemd  7462  nninfwlpoimlemg  7465  acfun  7513  pw1nel3  7540  sucpw1nel3  7542  ccfunen  7574  elni  7619  ltexpi  7648  enq0enq  7742  enq0ref  7744  enq0tr  7745  prarloclem3  7808  ltdfpr  7817  genpdflem  7818  genpassl  7835  genpassu  7836  nqprrnd  7854  nqprl  7862  nqpru  7863  ltexprlemopl  7912  ltexprlemopu  7914  ltexprlemdisj  7917  ltexprlemloc  7918  recexprlemdisj  7941  caucvgprprlemell  7996  caucvgprprlemelu  7997  suplocexprlemml  8027  suplocsrlemb  8117  opelcn  8137  elreal  8139  elreal2  8141  peano1nnnn  8163  axicn  8174  axaddf  8179  axmulf  8180  axprecex  8191  axpre-ltirr  8193  axpre-mulgt0  8198  axcaucvglemres  8210  axpre-suploc  8213  xrlenlt  8334  ltxrlt  8335  inelr  8854  reapcotr  8868  1nn  9244  elnnne0  9506  un0addcl  9525  un0mulcl  9526  elnnz  9583  elznn0nn  9587  elznn0  9588  elznn  9589  elz2  9645  zapne  9648  3halfnz  9671  prime  9673  raluz2  9907  rexuz2  9909  supinfneg  9923  infsupneg  9924  eluz2b2  9931  eluz2b3  9932  ublbneg  9941  elq  9950  qreccl  9970  elpq  9977  ralrp  10004  rexrp  10005  rpnegap  10015  ltxr  10104  xrnemnf  10106  xrltso  10125  icc0r  10255  divelunit  10331  fzprval  10412  fztpval  10413  elfz1b  10420  fz01or  10441  4fvwrd4  10470  fzolb  10484  fzolb2  10485  elfzo3  10494  fzouzsplit  10511  elfzo0z  10519  fzo0m  10527  fzind2  10581  ioo0  10615  ico0  10617  ioc0  10618  uzennn  10794  seq3f1olemp  10873  sseqn  11196  hashfibc  11200  iswrd  11219  caucvgre  11659  cvg1nlemcau  11662  resqrexlemex  11703  climeu  11974  fsum2dlemstep  12113  expcnv  12183  prodsnf  12271  fprod2dlemstep  12301  divides  12468  m1exp1  12580  divalgb  12604  bitsval2  12623  bitsmod  12635  bitscmp  12637  bezoutlemnewy  12685  bezoutlemmain  12687  bezoutlemex  12690  dfgcd2  12703  nnwosdc  12728  lcmgcdlem  12767  isprm2  12807  isprm3  12808  isprm4  12809  isprm5  12832  sqrt2irr  12852  oddpwdc  12864  pythagtriplem19  12973  pythagtrip  12974  pceu  12986  dvdsprmpweqnn  13027  4sqlem2  13080  4sqlem12  13093  dec5dvds2  13104  ennnfoneleminc  13151  ennnfonelemex  13154  ennnfonelemr  13163  ctiunct  13180  infpn2  13196  xpsfrnel  13546  xpsfrnel2  13548  gsum0g  13598  ismnd  13621  dfgrp2e  13730  dfgrp3me  13802  isnsg2  13909  eqger  13930  isabl2  14000  imasabl  14042  isrhm  14292  isrim  14303  isnzr2  14318  lss1d  14518  istps  14884  istps2  14885  isbasis2g  14897  tgval2  14903  txuni2  15108  tx1cn  15121  tx2cn  15122  uptx  15126  txdis1cn  15130  blres  15286  xmeterval  15287  xmeter  15288  isxms2  15304  isms2  15306  metrest  15358  qtopbasss  15373  dedekindicclemicc  15484  limcdifap  15514  plyrecj  15615  pilem1  15631  sincosq1lem  15677  mpodvdsmulf1o  15845  gausslemma2dlem1a  15918  gausslemma2dlem4  15924  lgsquadlem1  15937  lgsquadlem2  15938  2lgslem1b  15949  2sqlem1  15974  upgrex  16085  griedg0ssusgr  16233  clwwlkn1loopb  16402  clwwlknon2x  16417  decidr  16555  bdcuni  16633  bdcriota  16640  bdinex1  16656  bj-zfpair2  16667  bj-axun2  16672  bj-ssom  16693  ss1oel2o  16748  nninfsellemdc  16775  nninfsellemsuc  16777  nninfsellemqall  16780  trirec0xor  16816  iswomni0  16823