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  2797  issetf  2808  2gencl  2834  3gencl  2835  ceqsex2  2842  ceqsex3v  2844  ceqsex6v  2846  ceqsex8v  2847  gencbvex  2848  gencbval  2850  spc2gv  2895  eqvincf  2929  ceqsrex2v  2936  clel5  2941  elrab2  2963  ralab  2964  ralrab  2965  rexab  2966  rexrab  2967  ralab2  2968  rexab2  2970  eueq3dc  2978  morex  2988  euind  2991  reu2  2992  reu6  2993  rmo4  2997  reu4  2998  reu7  2999  rmo3f  3001  rmo4f  3002  rmoim  3005  2reuswapdc  3008  reuind  3009  2rmorex  3010  sbcco  3051  sbccomlem  3104  sbccom  3105  ra5  3119  rmo3  3122  csbco  3135  csbcow  3136  sbnfc2  3186  csbabg  3187  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  dfss  3212  dfss2f  3216  ss2ab  3293  dfdif3  3315  difeqri  3325  ddifstab  3337  raldifb  3345  uneqri  3347  ssequn2  3378  unss  3379  rexun  3385  ralunb  3386  elin2  3393  ineqri  3398  dfss1  3409  dfss5  3410  dfss4st  3438  ssddif  3439  difin  3442  indif  3448  difundi  3457  indifdir  3461  symdifxor  3471  inrab2  3478  rabun2  3484  reuun2  3488  0el  3515  rabeq0  3522  abeq0  3523  disjr  3542  disj1  3543  undif4  3555  uneqdifeqim  3578  r19.2m  3579  r19.3rm  3581  r19.9rmv  3584  raaan  3598  pwss  3666  dfpr2  3686  rexdifpr  3695  ralsnsg  3704  ralsns  3705  eltpg  3712  eldiftp  3713  ralprg  3718  rexprg  3719  raltpg  3720  rextpg  3721  snprc  3732  rabrsndc  3737  euabsn2  3738  eusn  3743  eldifsn  3798  ssdifsn  3799  rexdifsn  3803  eqsnm  3836  tpss  3839  snsssn  3842  prel12  3852  preqsn  3856  oprcl  3884  pwtpss  3888  eluniab  3903  elunirab  3904  unipr  3905  dfnfc2  3909  uniun  3910  uniin  3911  uni0b  3916  unissb  3921  elintab  3937  elintrab  3938  ssintab  3943  ssintrab  3949  intun  3957  intpr  3958  elrint  3966  iuncom4  3975  iuneq2  3984  dfiun2g  4000  ssiinf  4018  iundif2ss  4034  elriin  4039  iunxiun  4050  pwssb  4054  elpwpw  4055  iunpwss  4060  dfdisj2  4064  disjiun  4081  cbvopab1  4160  dftr5  4188  trint  4200  inex1  4221  inuni  4243  repizf2lem  4249  unidif0  4255  axpweq  4259  bnd2  4261  exmid01  4286  zfpair2  4298  exss  4317  elop  4321  opm  4324  otth  4332  copsex4g  4337  opeqsn  4343  opelopabsbALT  4351  brabga  4356  opelopabaf  4366  iunopab  4374  pwunss  4378  pocl  4398  frirrg  4445  elsuci  4498  elsucg  4499  sucel  4505  unisucg  4509  uniuni  4546  reusv3  4555  iunpw  4575  setindel  4634  elirr  4637  en2lp  4650  ordpwsucss  4663  zfregfr  4670  tfi  4678  peano2  4691  peano5  4694  elxp  4740  opelxp  4753  brxp  4754  rabxp  4761  opthprc  4775  brab2a  4777  opeliunxp  4779  xpundi  4780  xpundir  4781  elvvv  4787  brinxp  4792  brab2ga  4799  0xp  4804  ssrel2  4814  eqrelrel  4825  reliun  4846  reluni  4848  raliunxp  4869  rexiunxp  4870  ralxpf  4874  rexxpf  4875  iunxpf  4876  relop  4878  elco  4894  elcnv  4905  elcnv2  4906  dmin  4937  dmuni  4939  dmopab  4940  dmi  4944  dmmrnm  4949  rnopab  4977  elrnmpt1  4981  rncoeq  5004  resiexg  5056  restidsing  5067  dfima2  5076  dfima3  5077  elima2  5080  elima3  5081  imai  5090  elimasn  5101  epini  5105  dfse2  5107  cotr  5116  issref  5117  intasym  5119  asymref  5120  cnvopab  5136  cnvi  5139  cnvdif  5141  imainss  5150  rnxpid  5169  dfrel2  5185  dfrel3  5192  dmsnm  5200  rnsnm  5201  relsn2m  5205  dmsnopg  5206  cnvcnvsn  5211  elxp4  5222  elxp5  5223  cnvresima  5224  mptpreima  5228  dfco2  5234  coundi  5236  coundir  5237  imaco  5240  coiun  5244  coi1  5250  relssdmrn  5255  relrelss  5261  unixpm  5270  ressn  5275  cnviinm  5276  cnvpom  5277  cnvsom  5278  cbviota  5289  iotass  5302  eliota  5312  dffun2  5334  dffun4  5335  dffun7  5351  dffun8  5352  dffun9  5353  funopab  5359  funun  5368  funcnvsn  5372  fntpg  5383  funcnv2  5387  funcnv  5388  fun2cnv  5391  fncnv  5393  fun11  5394  fununi  5395  imadiflem  5406  imadif  5407  imainlem  5408  funimaexglem  5410  fnunsn  5436  fnres  5446  fnopabg  5453  mptfng  5455  mptun  5461  fun  5505  fcnvres  5517  dff12  5538  f1cnvcnv  5550  funforn  5563  dff1o2  5585  dff1o5  5589  f1orn  5590  resdif  5602  ffoss  5612  f11o  5613  f1o00  5616  fo00  5617  elfv  5633  fv3  5658  nfvres  5671  eqfnfv3  5742  fneqeql  5751  unpreima  5768  respreima  5771  dffo3  5790  dffo5  5792  f1ompt  5794  ffnfvf  5802  fmptco  5809  funopdmsn  5829  ftpg  5833  fnressn  5835  idref  5892  abrexco  5895  dff13  5904  dff13f  5906  fliftel  5929  isoini  5954  eusvobj2  5999  acexmidlema  6004  acexmidlemb  6005  acexmidlemph  6006  acexmidlem2  6010  oprabid  6045  brabvv  6062  dfoprab2  6063  eqoprab2b  6074  dmoprab  6097  rnoprab  6099  eloprabga  6103  mpomptx  6107  resoprab  6112  ffnov  6120  elrnmpo  6130  ralrnmpo  6131  rexrnmpo  6132  ovid  6133  ovi3  6154  ov6g  6155  foov  6164  opabex3d  6278  opabex3  6279  abexssex  6282  oprabex3  6286  oprabrexex2  6287  fmpo  6361  xporderlem  6391  f1od2  6395  mpoxopovel  6402  brtpos2  6412  dmtpos  6417  tpostpos  6425  tpossym  6437  tposoprab  6441  dfsmo2  6448  tfrlem7  6478  tfrlem9  6480  tfr1onlemaccex  6509  tfrcllemaccex  6522  tfrcldm  6524  frecabex  6559  el1o  6600  dif1o  6601  dfer2  6698  brdifun  6724  eqerlem  6728  qsid  6764  iinerm  6771  riinerm  6772  erinxp  6773  brecop  6789  eroveu  6790  erovlem  6791  ecopovsym  6795  mapval2  6842  mapsn  6854  elixp  6869  ixpeq2  6876  ixpin  6887  ixpiinm  6888  mptelixpg  6898  ixpsnf1o  6900  domen  6917  isfi  6929  en1  6968  modom2  6990  xpsnen  7000  xpcomco  7005  xpassen  7009  ssenen  7032  nneneq  7038  snnen2oprc  7041  ac6sfi  7082  exmidpw  7095  exmidpweq  7096  pw1dc1  7101  eldju  7261  djur  7262  eldju2ndl  7265  eldju2ndr  7266  finomni  7333  nninfwlporlemd  7365  nninfwlpoimlemg  7368  acfun  7415  pw1nel3  7442  sucpw1nel3  7444  ccfunen  7476  elni  7521  ltexpi  7550  enq0enq  7644  enq0ref  7646  enq0tr  7647  prarloclem3  7710  ltdfpr  7719  genpdflem  7720  genpassl  7737  genpassu  7738  nqprrnd  7756  nqprl  7764  nqpru  7765  ltexprlemopl  7814  ltexprlemopu  7816  ltexprlemdisj  7819  ltexprlemloc  7820  recexprlemdisj  7843  caucvgprprlemell  7898  caucvgprprlemelu  7899  suplocexprlemml  7929  suplocsrlemb  8019  opelcn  8039  elreal  8041  elreal2  8043  peano1nnnn  8065  axicn  8076  axaddf  8081  axmulf  8082  axprecex  8093  axpre-ltirr  8095  axpre-mulgt0  8100  axcaucvglemres  8112  axpre-suploc  8115  xrlenlt  8237  ltxrlt  8238  inelr  8757  reapcotr  8771  1nn  9147  elnnne0  9409  un0addcl  9428  un0mulcl  9429  elnnz  9482  elznn0nn  9486  elznn0  9487  elznn  9488  elz2  9544  zapne  9547  3halfnz  9570  prime  9572  raluz2  9806  rexuz2  9808  supinfneg  9822  infsupneg  9823  eluz2b2  9830  eluz2b3  9831  ublbneg  9840  elq  9849  qreccl  9869  elpq  9876  ralrp  9903  rexrp  9904  rpnegap  9914  ltxr  10003  xrnemnf  10005  xrltso  10024  icc0r  10154  divelunit  10230  fzprval  10310  fztpval  10311  elfz1b  10318  fz01or  10339  4fvwrd4  10368  fzolb  10382  fzolb2  10383  elfzo3  10392  fzouzsplit  10409  elfzo0z  10416  fzo0m  10424  fzind2  10478  ioo0  10512  ico0  10514  ioc0  10515  uzennn  10691  seq3f1olemp  10770  iswrd  11108  caucvgre  11535  cvg1nlemcau  11538  resqrexlemex  11579  climeu  11850  fsum2dlemstep  11988  expcnv  12058  prodsnf  12146  fprod2dlemstep  12176  divides  12343  m1exp1  12455  divalgb  12479  bitsval2  12498  bitsmod  12510  bitscmp  12512  bezoutlemnewy  12560  bezoutlemmain  12562  bezoutlemex  12565  dfgcd2  12578  nnwosdc  12603  lcmgcdlem  12642  isprm2  12682  isprm3  12683  isprm4  12684  isprm5  12707  sqrt2irr  12727  oddpwdc  12739  pythagtriplem19  12848  pythagtrip  12849  pceu  12861  dvdsprmpweqnn  12902  4sqlem2  12955  4sqlem12  12968  dec5dvds2  12979  ennnfoneleminc  13025  ennnfonelemex  13028  ennnfonelemr  13037  ctiunct  13054  infpn2  13070  xpsfrnel  13420  xpsfrnel2  13422  gsum0g  13472  ismnd  13495  dfgrp2e  13604  dfgrp3me  13676  isnsg2  13783  eqger  13804  isabl2  13874  imasabl  13916  isrhm  14165  isrim  14176  isnzr2  14191  lss1d  14390  istps  14749  istps2  14750  isbasis2g  14762  tgval2  14768  txuni2  14973  tx1cn  14986  tx2cn  14987  uptx  14991  txdis1cn  14995  blres  15151  xmeterval  15152  xmeter  15153  isxms2  15169  isms2  15171  metrest  15223  qtopbasss  15238  dedekindicclemicc  15349  limcdifap  15379  plyrecj  15480  pilem1  15496  sincosq1lem  15542  mpodvdsmulf1o  15707  gausslemma2dlem1a  15780  gausslemma2dlem4  15786  lgsquadlem1  15799  lgsquadlem2  15800  2lgslem1b  15811  2sqlem1  15836  upgrex  15947  griedg0ssusgr  16095  clwwlkn1loopb  16229  clwwlknon2x  16244  decidr  16342  bdcuni  16421  bdcriota  16428  bdinex1  16444  bj-zfpair2  16455  bj-axun2  16460  bj-ssom  16481  ss1oel2o  16536  nninfsellemdc  16562  nninfsellemsuc  16564  nninfsellemqall  16567  trirec0xor  16599  iswomni0  16605