Theorem bitri 183

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 119	. . 3 ⊢ (𝜑 → 𝜓)
3		bitri.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
4	2, 3	sylib 121	. 2 ⊢ (𝜑 → 𝜒)
5	3	biimpri 132	. . 3 ⊢ (𝜒 → 𝜓)
6	5, 1	sylibr 133	. 2 ⊢ (𝜒 → 𝜑)
7	4, 6	impbii 125	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bitr2i  184  bitr3i  185  bitr4i  186  bitrd  187  3bitri  205  3bitr2i  207  3bitr3i  209  3bitr4i  211  bibi12i  228  imbi12i  238  pm4.71r  388  biadan2  452  anbi2ci  455  anbi12i  456  anbi12ci  457  pm5.3  467  an42  577  xchbinx  672  mt2bi  674  orbi12i  754  or42  762  pm5.53  792  orddi  810  anddi  811  pm2.1dc  827  dcim  831  notnotrdc  833  dcnnOLD  839  rbaib  911  rbaibr  912  pm4.43  939  orbididc  943  pm5.75  952  3orass  971  3anass  972  3ancomb  976  3anan32  979  3anan12  980  anandi3  981  anandi3r  982  xordc  1382  falbitru  1407  19.26-2  1470  19.26-3an  1471  alrot3  1473  albiim  1475  2albiim  1476  19.27h  1548  19.27  1549  19.28h  1550  19.28  1551  nfalt  1566  aaanh  1574  aaan  1575  alinexa  1591  19.21-2  1655  nf2  1656  19.44  1670  19.45  1671  exrot3  1678  exrot4  1679  eeor  1683  sbcof2  1798  sbid2h  1837  19.23vv  1872  sbnv  1876  sblimv  1882  pm11.53  1883  19.41vv  1891  19.41vvv  1892  19.41vvvv  1893  exdistrv  1898  19.42vv  1899  19.42vvv  1900  19.42vvvv  1901  4exdistr  1904  cbvex4v  1918  eean  1919  sbn  1940  sbim  1941  sbor  1942  sban  1943  sbrim  1944  sblim  1945  sbbi  1947  sblbis  1948  sbrbis  1949  sbrbif  1950  sbco2d  1954  sbco2vd  1955  sbnf2  1969  2sb5  1971  2sb6  1972  sbcom2v  1973  sbcom2v2  1974  sbcom2  1975  sb6a  1976  2sb5rf  1977  2sb6rf  1978  sbalyz  1987  sbal  1988  sbal1yz  1989  sbex  1992  sbalv  1993  sbco4lem  1994  exsb  1996  2exsb  1997  eujust  2016  euf  2019  cbveu  2038  mor  2056  eu2  2058  mo4f  2074  eu4  2076  2exeu  2106  2eu4  2107  exists1  2110  abid  2153  eleq12i  2234  abeq2  2275  abeq2i  2277  clabel  2293  abid2f  2334  sbabel  2335  neeq12i  2353  neanior  2423  ralnex  2454  dfrex2dc  2457  ralinexa  2493  nfraldya  2501  nfrexdya  2502  r3al  2510  r19.26-2  2595  ralbiim  2600  ralnex2  2605  r19.43  2624  ralcomf  2627  rexcomf  2628  rexrot4  2632  reean  2634  3reeanv  2636  rabbi  2643  cbvralf  2685  cbvrexf  2686  cbvreu  2690  cbvral2vw  2703  cbvrex2vw  2704  cbvral2v  2705  cbvrex2v  2706  cbvral3v  2707  cbvralsv  2708  cbvrexsv  2709  sbralie  2710  rabeq2i  2723  issetf  2733  2gencl  2759  3gencl  2760  ceqsex2  2766  ceqsex3v  2768  ceqsex6v  2770  ceqsex8v  2771  gencbvex  2772  gencbval  2774  spc2gv  2817  eqvincf  2851  ceqsrex2v  2858  clel5  2863  elrab2  2885  ralab  2886  ralrab  2887  rexab  2888  rexrab  2889  ralab2  2890  rexab2  2892  eueq3dc  2900  morex  2910  euind  2913  reu2  2914  reu6  2915  rmo4  2919  reu4  2920  reu7  2921  rmo3f  2923  rmo4f  2924  rmoim  2927  2reuswapdc  2930  reuind  2931  2rmorex  2932  sbcco  2972  sbccomlem  3025  sbccom  3026  ra5  3039  rmo3  3042  csbco  3055  csbcow  3056  sbnfc2  3105  csbabg  3106  cbvralcsf  3107  cbvrexcsf  3108  cbvreucsf  3109  dfss  3130  dfss2f  3133  ss2ab  3210  dfdif3  3232  difeqri  3242  ddifstab  3254  raldifb  3262  uneqri  3264  ssequn2  3295  unss  3296  rexun  3302  ralunb  3303  elin2  3310  ineqri  3315  dfss1  3326  dfss5  3327  dfss4st  3355  ssddif  3356  difin  3359  indif  3365  difundi  3374  indifdir  3378  symdifxor  3388  inrab2  3395  rabun2  3401  reuun2  3405  0el  3431  rabeq0  3438  abeq0  3439  disjr  3458  disj1  3459  undif4  3471  uneqdifeqim  3494  r19.2m  3495  r19.3rm  3497  r19.9rmv  3500  raaan  3515  pwss  3575  dfpr2  3595  rexdifpr  3604  ralsnsg  3613  ralsns  3614  eltpg  3621  eldiftp  3622  ralprg  3627  rexprg  3628  raltpg  3629  rextpg  3630  snprc  3641  rabrsndc  3644  euabsn2  3645  eusn  3650  eldifsn  3703  ssdifsn  3704  rexdifsn  3708  eqsnm  3735  tpss  3738  snsssn  3741  prel12  3751  preqsn  3755  oprcl  3782  pwtpss  3786  eluniab  3801  elunirab  3802  unipr  3803  dfnfc2  3807  uniun  3808  uniin  3809  uni0b  3814  unissb  3819  elintab  3835  elintrab  3836  ssintab  3841  ssintrab  3847  intun  3855  intpr  3856  elrint  3864  iuncom4  3873  iuneq2  3882  dfiun2g  3898  ssiinf  3915  iundif2ss  3931  elriin  3936  iunxiun  3947  pwssb  3951  elpwpw  3952  iunpwss  3957  dfdisj2  3961  disjiun  3977  cbvopab1  4055  dftr5  4083  trint  4095  inex1  4116  inuni  4134  repizf2lem  4140  unidif0  4146  axpweq  4150  bnd2  4152  exmid01  4177  zfpair2  4188  exss  4205  elop  4209  opm  4212  otth  4220  copsex4g  4225  opeqsn  4230  opelopabsbALT  4237  brabga  4242  opelopabaf  4251  iunopab  4259  pwunss  4261  pocl  4281  frirrg  4328  elsuci  4381  elsucg  4382  sucel  4388  unisucg  4392  uniuni  4429  reusv3  4438  iunpw  4458  setindel  4515  elirr  4518  en2lp  4531  ordpwsucss  4544  zfregfr  4551  tfi  4559  peano2  4572  peano5  4575  elxp  4621  opelxp  4634  brxp  4635  rabxp  4641  opthprc  4655  brab2a  4657  opeliunxp  4659  xpundi  4660  xpundir  4661  elvvv  4667  brinxp  4672  brab2ga  4679  0xp  4684  ssrel2  4694  eqrelrel  4705  reliun  4725  reluni  4727  raliunxp  4745  rexiunxp  4746  ralxpf  4750  rexxpf  4751  iunxpf  4752  relop  4754  elco  4770  elcnv  4781  elcnv2  4782  dmin  4812  dmuni  4814  dmopab  4815  dmi  4819  dmmrnm  4823  rnopab  4851  elrnmpt1  4855  rncoeq  4877  resiexg  4929  dfima2  4948  dfima3  4949  elima2  4952  elima3  4953  imai  4960  elimasn  4971  epini  4975  dfse2  4977  cotr  4985  issref  4986  intasym  4988  asymref  4989  cnvopab  5005  cnvi  5008  cnvdif  5010  imainss  5019  rnxpid  5038  dfrel2  5054  dfrel3  5061  dmsnm  5069  rnsnm  5070  relsn2m  5074  dmsnopg  5075  cnvcnvsn  5080  elxp4  5091  elxp5  5092  cnvresima  5093  mptpreima  5097  dfco2  5103  coundi  5105  coundir  5106  imaco  5109  coiun  5113  coi1  5119  relssdmrn  5124  relrelss  5130  unixpm  5139  ressn  5144  cnviinm  5145  cnvpom  5146  cnvsom  5147  cbviota  5158  iotass  5170  dffun2  5198  dffun4  5199  dffun7  5215  dffun8  5216  dffun9  5217  funopab  5223  funun  5232  funcnvsn  5233  fntpg  5244  funcnv2  5248  funcnv  5249  fun2cnv  5252  fncnv  5254  fun11  5255  fununi  5256  imadiflem  5267  imadif  5268  imainlem  5269  funimaexglem  5271  fnunsn  5295  fnres  5304  fnopabg  5311  mptfng  5313  mptun  5319  fun  5360  fcnvres  5371  dff12  5392  f1cnvcnv  5404  funforn  5417  dff1o2  5437  dff1o5  5441  f1orn  5442  resdif  5454  ffoss  5464  f11o  5465  f1o00  5467  fo00  5468  elfv  5484  fv3  5509  nfvres  5519  eqfnfv3  5585  fneqeql  5593  unpreima  5610  respreima  5613  dffo3  5632  dffo5  5634  f1ompt  5636  ffnfvf  5644  fmptco  5651  ftpg  5669  fnressn  5671  idref  5725  abrexco  5727  dff13  5736  dff13f  5738  fliftel  5761  isoini  5786  eusvobj2  5828  acexmidlema  5833  acexmidlemb  5834  acexmidlemph  5835  acexmidlem2  5839  oprabid  5874  brabvv  5888  dfoprab2  5889  eqoprab2b  5900  dmoprab  5923  rnoprab  5925  eloprabga  5929  mpomptx  5933  resoprab  5938  ffnov  5946  elrnmpo  5955  ralrnmpo  5956  rexrnmpo  5957  ovid  5958  ovi3  5978  ov6g  5979  foov  5988  opabex3d  6089  opabex3  6090  abexssex  6093  oprabex3  6097  oprabrexex2  6098  fmpo  6169  xporderlem  6199  f1od2  6203  mpoxopovel  6209  brtpos2  6219  dmtpos  6224  tpostpos  6232  tpossym  6244  tposoprab  6248  dfsmo2  6255  tfrlem7  6285  tfrlem9  6287  tfr1onlemaccex  6316  tfrcllemaccex  6329  tfrcldm  6331  frecabex  6366  el1o  6405  dif1o  6406  dfer2  6502  brdifun  6528  eqerlem  6532  qsid  6566  iinerm  6573  riinerm  6574  erinxp  6575  brecop  6591  eroveu  6592  erovlem  6593  ecopovsym  6597  mapval2  6644  mapsn  6656  elixp  6671  ixpeq2  6678  ixpin  6689  ixpiinm  6690  mptelixpg  6700  ixpsnf1o  6702  domen  6717  isfi  6727  en1  6765  xpsnen  6787  xpcomco  6792  xpassen  6796  ssenen  6817  nneneq  6823  snnen2oprc  6826  ac6sfi  6864  exmidpw  6874  exmidpweq  6875  pw1dc1  6879  eldju  7033  djur  7034  eldju2ndl  7037  eldju2ndr  7038  finomni  7104  acfun  7163  pw1nel3  7187  sucpw1nel3  7189  ccfunen  7205  elni  7249  ltexpi  7278  enq0enq  7372  enq0ref  7374  enq0tr  7375  prarloclem3  7438  ltdfpr  7447  genpdflem  7448  genpassl  7465  genpassu  7466  nqprrnd  7484  nqprl  7492  nqpru  7493  ltexprlemopl  7542  ltexprlemopu  7544  ltexprlemdisj  7547  ltexprlemloc  7548  recexprlemdisj  7571  caucvgprprlemell  7626  caucvgprprlemelu  7627  suplocexprlemml  7657  suplocsrlemb  7747  opelcn  7767  elreal  7769  elreal2  7771  peano1nnnn  7793  axicn  7804  axaddf  7809  axmulf  7810  axprecex  7821  axpre-ltirr  7823  axpre-mulgt0  7828  axcaucvglemres  7840  axpre-suploc  7843  xrlenlt  7963  ltxrlt  7964  inelr  8482  reapcotr  8496  1nn  8868  elnnne0  9128  un0addcl  9147  un0mulcl  9148  elnnz  9201  elznn0nn  9205  elznn0  9206  elznn  9207  elz2  9262  zapne  9265  3halfnz  9288  prime  9290  raluz2  9517  rexuz2  9519  supinfneg  9533  infsupneg  9534  eluz2b2  9541  eluz2b3  9542  ublbneg  9551  elq  9560  qreccl  9580  elpq  9586  ralrp  9611  rexrp  9612  rpnegap  9622  ltxr  9711  xrnemnf  9713  xrltso  9732  icc0r  9862  divelunit  9938  fzprval  10017  fztpval  10018  elfz1b  10025  fz01or  10046  4fvwrd4  10075  fzolb  10088  fzolb2  10089  elfzo3  10098  fzouzsplit  10114  elfzo0z  10119  fzo0m  10126  fzind2  10174  ioo0  10195  ico0  10197  ioc0  10198  uzennn  10371  seq3f1olemp  10437  caucvgre  10923  cvg1nlemcau  10926  resqrexlemex  10967  climeu  11237  fsum2dlemstep  11375  expcnv  11445  prodsnf  11533  fprod2dlemstep  11563  divides  11729  m1exp1  11838  divalgb  11862  bezoutlemnewy  11929  bezoutlemmain  11931  bezoutlemex  11934  dfgcd2  11947  nnwosdc  11972  lcmgcdlem  12009  isprm2  12049  isprm3  12050  isprm4  12051  isprm5  12074  sqrt2irr  12094  oddpwdc  12106  pythagtriplem19  12214  pythagtrip  12215  pceu  12227  dvdsprmpweqnn  12267  4sqlem2  12319  ennnfoneleminc  12344  ennnfonelemex  12347  ennnfonelemr  12356  ctiunct  12373  infpn2  12389  istps  12670  istps2  12671  isbasis2g  12683  tgval2  12691  txuni2  12896  tx1cn  12909  tx2cn  12910  uptx  12914  txdis1cn  12918  blres  13074  xmeterval  13075  xmeter  13076  isxms2  13092  isms2  13094  metrest  13146  qtopbasss  13161  dedekindicclemicc  13250  limcdifap  13271  pilem1  13340  sincosq1lem  13386  2sqlem1  13590  decidr  13677  bdcuni  13758  bdcriota  13765  bdinex1  13781  bj-zfpair2  13792  bj-axun2  13797  bj-ssom  13818  ss1oel2o  13873  nninfsellemdc  13890  nninfsellemsuc  13892  nninfsellemqall  13895  trirec0xor  13924  iswomni0  13930