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  1939  sblimv  1946  pm11.53  1947  19.41vv  1955  19.41vvv  1956  19.41vvvv  1957  exdistrv  1962  19.42vv  1963  19.42vvv  1964  19.42vvvv  1965  4exdistr  1968  cbvex4v  1986  eean  1987  sbn  2008  sbim  2009  sbor  2010  sban  2011  sbrim  2012  sblim  2013  sbbi  2015  sblbis  2016  sbrbis  2017  sbrbif  2018  sbco2d  2022  sbco2vd  2023  sbnf2  2037  2sb5  2039  2sb6  2040  sbcom2v  2041  sbcom2v2  2042  sbcom2  2043  sb6a  2044  2sb5rf  2045  2sb6rf  2046  sbalyz  2055  sbal  2056  sbal1yz  2057  sbex  2060  sbalv  2061  sbco4lem  2062  exsb  2064  2exsb  2065  eujust  2084  euf  2087  cbveu  2106  mor  2125  eu2  2127  mo4f  2143  eu4  2145  2exeu  2175  2eu4  2176  exists1  2179  abid  2222  eleq12i  2302  abeq2  2343  abeq2i  2345  abbib  2352  clabel  2363  eqabb  2370  abid2f  2412  sbabel  2413  neeq12i  2431  neanior  2501  ralnex  2532  dfrex2dc  2535  ralinexa  2571  nfraldya  2579  nfrexdya  2580  r3al  2588  r19.26-2  2674  ralbiim  2679  ralnex2  2684  r19.43  2703  ralcomf  2706  rexcomf  2707  ralrot3  2710  rexrot4  2712  reean  2714  3reeanv  2716  reqabi  2722  rabbi  2724  cbvralf  2771  cbvrexf  2772  cbvreu  2778  cbvral2vw  2791  cbvrex2vw  2792  cbvral2v  2793  cbvrex2v  2794  cbvral3v  2795  cbvralsv  2796  cbvrexsv  2797  sbralie  2798  rabeq2i  2812  issetf  2823  2gencl  2849  3gencl  2850  ceqsex2  2857  ceqsex3v  2859  ceqsex6v  2861  ceqsex8v  2862  gencbvex  2863  gencbval  2865  spc2gv  2910  eqvincf  2945  ceqsrex2v  2952  clel5  2957  elrab2  2979  ralab  2980  ralrab  2981  rexab  2982  rexrab  2983  ralab2  2984  rexab2  2986  eueq3dc  2994  morex  3004  euind  3007  reu2  3008  reu6  3009  rmo4  3013  reu4  3014  reu7  3015  rmo3f  3017  rmo4f  3018  rmoim  3021  2reuswapdc  3024  reuind  3025  2rmorex  3026  sbcco  3067  sbccomlem  3120  sbccom  3121  ra5  3135  rmo3  3138  csbco  3151  csbcow  3152  sbnfc2  3202  csbabg  3203  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  dfss  3228  dfssf  3232  dfss2f  3233  ss2ab  3310  dfdif3  3333  difeqri  3343  ddifstab  3355  raldifb  3363  uneqri  3365  ssequn2  3396  unss  3397  rexun  3403  ralunb  3404  elin2  3411  ineqri  3418  dfss1  3429  dfss5  3430  dfss4st  3458  ssddif  3459  difin  3462  indif  3468  difundi  3477  indifdir  3481  symdifxor  3491  inrab2  3498  rabun2  3504  reuun2  3508  0el  3535  rabeq0  3542  abeq0  3543  disjr  3562  disj1  3563  undif4  3575  uneqdifeqim  3599  r19.2m  3600  r19.3rm  3602  r19.9rmv  3605  raaan  3619  pwss  3693  dfpr2  3713  rexdifpr  3722  ralsnsg  3731  ralsns  3732  eltpg  3739  eldiftp  3740  ralprg  3745  rexprg  3746  raltpg  3747  rextpg  3748  snprc  3759  rabrsndc  3764  euabsn2  3765  eusn  3770  eldifsn  3825  ssdifsn  3826  rexdifsn  3830  eqsnm  3864  tpss  3867  snsssn  3870  prel12  3880  preqsn  3884  oprcl  3912  pwtpss  3916  eluniab  3931  elunirab  3932  unipr  3933  dfnfc2  3937  uniun  3938  uniin  3939  uni0b  3944  unissb  3949  elintab  3965  elintrab  3966  ssintab  3971  ssintrab  3977  intun  3985  intpr  3986  elrint  3994  iuncom4  4003  iuneq2  4012  dfiun2g  4028  ssiinf  4046  iundif2ss  4062  elriin  4067  iunxiun  4078  pwssb  4082  elpwpw  4083  iunpwss  4088  dfdisj2  4092  disjiun  4109  cbvopab1  4188  dftr5  4216  trint  4228  inex1  4249  inuni  4272  repizf2lem  4279  unidif0  4285  axpweq  4289  bnd2  4291  exmid01  4316  zfpair2  4328  exss  4348  elop  4352  opm  4355  otth  4363  copsex4g  4368  opeqsn  4374  opelopabsbALT  4382  brabga  4387  opelopabaf  4397  iunopab  4405  pwunss  4409  pocl  4429  frirrg  4476  elsuci  4529  elsucg  4530  sucel  4536  unisucg  4540  uniuni  4577  reusv3  4586  iunpw  4606  setindel  4665  elirr  4668  en2lp  4681  ordpwsucss  4694  zfregfr  4701  tfi  4709  peano2  4722  peano5  4725  elxp  4771  opelxp  4784  brxp  4785  rabxp  4792  opthprc  4806  brab2a  4808  opeliunxp  4810  xpundi  4811  xpundir  4812  elvvv  4818  brinxp  4823  brab2ga  4830  0xp  4835  ssrel2  4845  eqrelrel  4856  reliun  4878  reluni  4880  raliunxp  4901  rexiunxp  4902  ralxpf  4906  rexxpf  4907  iunxpf  4908  relop  4910  elco  4926  elcnv  4937  elcnv2  4938  dmin  4969  dmuni  4971  dmopab  4972  dmi  4976  dmmrnm  4981  rnopab  5009  elrnmpt1  5013  rncoeq  5036  resiexg  5088  restidsing  5099  dfima2  5108  dfima3  5109  elima2  5112  elima3  5113  imai  5123  elimasn  5134  epini  5138  dfse2  5140  cotr  5149  issref  5150  intasym  5152  asymref  5153  cnvopab  5169  cnvi  5172  cnvdif  5174  imainss  5183  rnxpid  5202  dfrel2  5218  dfrel3  5225  dmsnm  5233  rnsnm  5234  relsn2m  5238  dmsnopg  5239  cnvcnvsn  5244  elxp4  5255  elxp5  5256  cnvresima  5257  mptpreima  5261  dfco2  5267  coundi  5269  coundir  5270  imaco  5273  coiun  5277  coi1  5283  relssdmrn  5288  relrelss  5294  unixpm  5303  ressn  5308  cnviinm  5309  cnvpom  5310  cnvsom  5311  cbviota  5322  iotass  5335  eliota  5345  dffun2  5367  dffun4  5368  dffun7  5384  dffun8  5385  dffun9  5386  funopab  5392  funun  5402  funcnvsn  5406  fntpg  5417  funcnv2  5421  funcnv  5422  fun2cnv  5425  fncnv  5427  fun11  5428  fununi  5429  imadiflem  5440  imadif  5441  imainlem  5442  funimaexglem  5444  fnunsn  5470  fnres  5480  fnopabg  5487  mptfng  5489  mptun  5495  fun  5541  fcnvres  5555  dff12  5577  f1cnvcnv  5589  funforn  5602  dff1o2  5624  dff1o5  5628  f1orn  5629  resdif  5641  ffoss  5652  f11o  5653  f1o00  5656  fo00  5657  elfv  5673  fv3  5698  nfvres  5711  eqfnfv3  5782  fneqeql  5791  unpreima  5807  respreima  5810  dffo3  5829  dffo5  5831  f1ompt  5833  ffnfvf  5841  fmptco  5848  funopdmsn  5869  ftpg  5873  fnressn  5875  idref  5935  abrexco  5938  dff13  5947  dff13f  5949  fliftel  5972  isoini  5997  eusvobj2  6044  acexmidlema  6049  acexmidlemb  6050  acexmidlemph  6051  acexmidlem2  6055  oprabid  6090  brabvv  6107  dfoprab2  6108  eqoprab2b  6119  dmoprab  6142  rnoprab  6144  eloprabga  6148  mpomptx  6152  resoprab  6157  ffnov  6165  elrnmpo  6175  ralrnmpo  6176  rexrnmpo  6177  ovid  6178  ovi3  6199  ov6g  6200  foov  6209  opabex3d  6323  opabex3  6324  abexssex  6327  oprabex3  6335  oprabrexex2  6336  fmpo  6410  xporderlem  6440  f1od2  6444  mpoxopovel  6485  brtpos2  6495  dmtpos  6500  tpostpos  6508  tpossym  6520  tposoprab  6524  dfsmo2  6531  tfrlem7  6561  tfrlem9  6563  tfr1onlemaccex  6592  tfrcllemaccex  6605  tfrcldm  6607  frecabex  6642  el1o  6683  dif1o  6684  dfer2  6781  brdifun  6807  eqerlem  6811  qsid  6847  iinerm  6854  riinerm  6855  erinxp  6856  brecop  6872  eroveu  6873  erovlem  6874  ecopovsym  6878  mapval2  6925  mapsn  6938  elixp  6953  ixpeq2  6960  ixpin  6971  ixpiinm  6972  mptelixpg  6982  ixpsnf1o  6984  domen  7001  isfi  7013  en1  7052  modom2  7075  xpsnen  7085  xpcomco  7090  xpassen  7094  ssenen  7118  nneneq  7124  snnen2oprc  7127  ac6sfi  7168  exmidpw  7181  exmidpweq  7182  pw1dc1  7187  elfpw  7228  eldju  7372  djur  7373  eldju2ndl  7376  eldju2ndr  7377  finomni  7444  nninfwlporlemd  7476  nninfwlpoimlemg  7479  acfun  7527  pw1nel3  7554  sucpw1nel3  7556  ccfunen  7594  elni  7639  ltexpi  7668  enq0enq  7762  enq0ref  7764  enq0tr  7765  prarloclem3  7828  ltdfpr  7837  genpdflem  7838  genpassl  7855  genpassu  7856  nqprrnd  7874  nqprl  7882  nqpru  7883  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemdisj  7937  ltexprlemloc  7938  recexprlemdisj  7961  caucvgprprlemell  8016  caucvgprprlemelu  8017  suplocexprlemml  8047  suplocsrlemb  8137  opelcn  8157  elreal  8159  elreal2  8161  peano1nnnn  8183  axicn  8194  axaddf  8199  axmulf  8200  axprecex  8211  axpre-ltirr  8213  axpre-mulgt0  8218  axcaucvglemres  8230  axpre-suploc  8233  xrlenlt  8354  ltxrlt  8355  inelr  8876  reapcotr  8890  1nn  9268  elnnne0  9530  un0addcl  9549  un0mulcl  9550  elnnz  9607  elznn0nn  9611  elznn0  9612  elznn  9613  elz2  9669  zapne  9672  3halfnz  9696  prime  9698  raluz2  9932  rexuz2  9934  supinfneg  9948  infsupneg  9949  eluz2b2  9956  eluz2b3  9957  ublbneg  9966  elq  9975  qreccl  9995  elpq  10002  ralrp  10029  rexrp  10030  rpnegap  10040  ltxr  10130  xrnemnf  10132  xrltso  10151  icc0r  10281  divelunit  10357  fzprval  10441  fztpval  10442  elfz1b  10449  fz01or  10470  4fvwrd4  10499  fzolb  10513  fzolb2  10514  elfzo3  10523  fzouzsplit  10540  elfzo0z  10548  fzo0m  10556  fzind2  10610  infssfzcldc  10621  infssfzledc  10622  ioo0  10646  ico0  10648  ioc0  10649  uzennn  10825  seq3f1olemp  10904  sseqn  11231  hashfibc  11235  iswrd  11254  caucvgre  11694  cvg1nlemcau  11697  resqrexlemex  11738  climeu  12009  fsum2dlemstep  12148  expcnv  12218  prodsnf  12306  fprod2dlemstep  12336  divides  12503  m1exp1  12615  divalgb  12639  bitsval2  12658  bitsmod  12670  bitscmp  12672  bezoutlemnewy  12720  bezoutlemmain  12722  bezoutlemex  12725  dfgcd2  12738  nnwosdc  12763  lcmgcdlem  12802  isprm2  12842  isprm3  12843  isprm4  12844  isprm5  12867  sqrt2irr  12887  oddpwdc  12899  pythagtriplem19  13008  pythagtrip  13009  pceu  13021  dvdsprmpweqnn  13062  4sqlem2  13115  4sqlem12  13128  dec5dvds2  13139  ballotfilemodife  13187  ballotfilem4  13188  ennnfoneleminc  13249  ennnfonelemex  13252  ennnfonelemr  13261  ctiunct  13278  infpn2  13294  xpsfrnel  13611  xpsfrnel2  13613  gsum0g  13662  ismnd  13683  dfgrp2e  13786  dfgrp3me  13858  isnsg2  13959  eqger  13980  isabl2  14050  imasabl  14092  isrhm  14406  isrim  14417  isnzr2  14432  drngprop  14558  lss1d  14660  istps  15026  istps2  15027  isbasis2g  15039  tgval2  15045  txuni2  15250  tx1cn  15263  tx2cn  15264  uptx  15268  txdis1cn  15272  blres  15428  xmeterval  15429  xmeter  15430  isxms2  15446  isms2  15448  metrest  15500  qtopbasss  15515  dedekindicclemicc  15626  limcdifap  15656  plyrecj  15757  pilem1  15773  sincosq1lem  15819  mpodvdsmulf1o  15987  gausslemma2dlem1a  16060  gausslemma2dlem4  16066  lgsquadlem1  16079  lgsquadlem2  16080  2lgslem1b  16091  2sqlem1  16116  upgrex  16227  griedg0ssusgr  16375  clwwlkn1loopb  16544  clwwlknon2x  16559  decidr  16707  bdcuni  16785  bdcriota  16792  bdinex1  16808  bj-zfpair2  16819  bj-axun2  16824  bj-ssom  16845  ss1oel2o  16900  nninfsellemdc  16927  nninfsellemsuc  16929  nninfsellemqall  16932  trirec0xor  16968  iswomni0  16975