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  453  anbi2ci  456  anbi12i  457  anbi12ci  458  bianassc  467  pm5.3  472  an42  582  xchbinx  677  mt2bi  679  orbi12i  759  or42  767  pm5.53  797  orddi  815  anddi  816  pm2.1dc  832  dcim  836  notnotrdc  838  dcnnOLD  844  rbaib  916  rbaibr  917  pm4.43  944  orbididc  948  pm5.75  957  3orass  976  3anass  977  3ancomb  981  3anan32  984  3anan12  985  anandi3  986  anandi3r  987  xordc  1387  falbitru  1412  19.26-2  1475  19.26-3an  1476  alrot3  1478  albiim  1480  2albiim  1481  19.27h  1553  19.27  1554  19.28h  1555  19.28  1556  nfalt  1571  aaanh  1579  aaan  1580  alinexa  1596  19.21-2  1660  nf2  1661  19.44  1675  19.45  1676  exrot3  1683  exrot4  1684  eeor  1688  sbcof2  1803  sbid2h  1842  19.23vv  1877  sbnv  1881  sblimv  1887  pm11.53  1888  19.41vv  1896  19.41vvv  1897  19.41vvvv  1898  exdistrv  1903  19.42vv  1904  19.42vvv  1905  19.42vvvv  1906  4exdistr  1909  cbvex4v  1923  eean  1924  sbn  1945  sbim  1946  sbor  1947  sban  1948  sbrim  1949  sblim  1950  sbbi  1952  sblbis  1953  sbrbis  1954  sbrbif  1955  sbco2d  1959  sbco2vd  1960  sbnf2  1974  2sb5  1976  2sb6  1977  sbcom2v  1978  sbcom2v2  1979  sbcom2  1980  sb6a  1981  2sb5rf  1982  2sb6rf  1983  sbalyz  1992  sbal  1993  sbal1yz  1994  sbex  1997  sbalv  1998  sbco4lem  1999  exsb  2001  2exsb  2002  eujust  2021  euf  2024  cbveu  2043  mor  2061  eu2  2063  mo4f  2079  eu4  2081  2exeu  2111  2eu4  2112  exists1  2115  abid  2158  eleq12i  2238  abeq2  2279  abeq2i  2281  clabel  2297  abid2f  2338  sbabel  2339  neeq12i  2357  neanior  2427  ralnex  2458  dfrex2dc  2461  ralinexa  2497  nfraldya  2505  nfrexdya  2506  r3al  2514  r19.26-2  2599  ralbiim  2604  ralnex2  2609  r19.43  2628  ralcomf  2631  rexcomf  2632  rexrot4  2636  reean  2638  3reeanv  2640  rabbi  2647  cbvralf  2689  cbvrexf  2690  cbvreu  2694  cbvral2vw  2707  cbvrex2vw  2708  cbvral2v  2709  cbvrex2v  2710  cbvral3v  2711  cbvralsv  2712  cbvrexsv  2713  sbralie  2714  rabeq2i  2727  issetf  2737  2gencl  2763  3gencl  2764  ceqsex2  2770  ceqsex3v  2772  ceqsex6v  2774  ceqsex8v  2775  gencbvex  2776  gencbval  2778  spc2gv  2821  eqvincf  2855  ceqsrex2v  2862  clel5  2867  elrab2  2889  ralab  2890  ralrab  2891  rexab  2892  rexrab  2893  ralab2  2894  rexab2  2896  eueq3dc  2904  morex  2914  euind  2917  reu2  2918  reu6  2919  rmo4  2923  reu4  2924  reu7  2925  rmo3f  2927  rmo4f  2928  rmoim  2931  2reuswapdc  2934  reuind  2935  2rmorex  2936  sbcco  2976  sbccomlem  3029  sbccom  3030  ra5  3043  rmo3  3046  csbco  3059  csbcow  3060  sbnfc2  3109  csbabg  3110  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  dfss  3135  dfss2f  3138  ss2ab  3215  dfdif3  3237  difeqri  3247  ddifstab  3259  raldifb  3267  uneqri  3269  ssequn2  3300  unss  3301  rexun  3307  ralunb  3308  elin2  3315  ineqri  3320  dfss1  3331  dfss5  3332  dfss4st  3360  ssddif  3361  difin  3364  indif  3370  difundi  3379  indifdir  3383  symdifxor  3393  inrab2  3400  rabun2  3406  reuun2  3410  0el  3436  rabeq0  3443  abeq0  3444  disjr  3463  disj1  3464  undif4  3476  uneqdifeqim  3499  r19.2m  3500  r19.3rm  3502  r19.9rmv  3505  raaan  3520  pwss  3580  dfpr2  3600  rexdifpr  3609  ralsnsg  3618  ralsns  3619  eltpg  3626  eldiftp  3627  ralprg  3632  rexprg  3633  raltpg  3634  rextpg  3635  snprc  3646  rabrsndc  3649  euabsn2  3650  eusn  3655  eldifsn  3708  ssdifsn  3709  rexdifsn  3713  eqsnm  3740  tpss  3743  snsssn  3746  prel12  3756  preqsn  3760  oprcl  3787  pwtpss  3791  eluniab  3806  elunirab  3807  unipr  3808  dfnfc2  3812  uniun  3813  uniin  3814  uni0b  3819  unissb  3824  elintab  3840  elintrab  3841  ssintab  3846  ssintrab  3852  intun  3860  intpr  3861  elrint  3869  iuncom4  3878  iuneq2  3887  dfiun2g  3903  ssiinf  3920  iundif2ss  3936  elriin  3941  iunxiun  3952  pwssb  3956  elpwpw  3957  iunpwss  3962  dfdisj2  3966  disjiun  3982  cbvopab1  4060  dftr5  4088  trint  4100  inex1  4121  inuni  4139  repizf2lem  4145  unidif0  4151  axpweq  4155  bnd2  4157  exmid01  4182  zfpair2  4193  exss  4210  elop  4214  opm  4217  otth  4225  copsex4g  4230  opeqsn  4235  opelopabsbALT  4242  brabga  4247  opelopabaf  4256  iunopab  4264  pwunss  4266  pocl  4286  frirrg  4333  elsuci  4386  elsucg  4387  sucel  4393  unisucg  4397  uniuni  4434  reusv3  4443  iunpw  4463  setindel  4520  elirr  4523  en2lp  4536  ordpwsucss  4549  zfregfr  4556  tfi  4564  peano2  4577  peano5  4580  elxp  4626  opelxp  4639  brxp  4640  rabxp  4646  opthprc  4660  brab2a  4662  opeliunxp  4664  xpundi  4665  xpundir  4666  elvvv  4672  brinxp  4677  brab2ga  4684  0xp  4689  ssrel2  4699  eqrelrel  4710  reliun  4730  reluni  4732  raliunxp  4750  rexiunxp  4751  ralxpf  4755  rexxpf  4756  iunxpf  4757  relop  4759  elco  4775  elcnv  4786  elcnv2  4787  dmin  4817  dmuni  4819  dmopab  4820  dmi  4824  dmmrnm  4828  rnopab  4856  elrnmpt1  4860  rncoeq  4882  resiexg  4934  dfima2  4953  dfima3  4954  elima2  4957  elima3  4958  imai  4965  elimasn  4976  epini  4980  dfse2  4982  cotr  4990  issref  4991  intasym  4993  asymref  4994  cnvopab  5010  cnvi  5013  cnvdif  5015  imainss  5024  rnxpid  5043  dfrel2  5059  dfrel3  5066  dmsnm  5074  rnsnm  5075  relsn2m  5079  dmsnopg  5080  cnvcnvsn  5085  elxp4  5096  elxp5  5097  cnvresima  5098  mptpreima  5102  dfco2  5108  coundi  5110  coundir  5111  imaco  5114  coiun  5118  coi1  5124  relssdmrn  5129  relrelss  5135  unixpm  5144  ressn  5149  cnviinm  5150  cnvpom  5151  cnvsom  5152  cbviota  5163  iotass  5175  eliota  5184  dffun2  5206  dffun4  5207  dffun7  5223  dffun8  5224  dffun9  5225  funopab  5231  funun  5240  funcnvsn  5241  fntpg  5252  funcnv2  5256  funcnv  5257  fun2cnv  5260  fncnv  5262  fun11  5263  fununi  5264  imadiflem  5275  imadif  5276  imainlem  5277  funimaexglem  5279  fnunsn  5303  fnres  5312  fnopabg  5319  mptfng  5321  mptun  5327  fun  5368  fcnvres  5379  dff12  5400  f1cnvcnv  5412  funforn  5425  dff1o2  5445  dff1o5  5449  f1orn  5450  resdif  5462  ffoss  5472  f11o  5473  f1o00  5475  fo00  5476  elfv  5492  fv3  5517  nfvres  5527  eqfnfv3  5593  fneqeql  5601  unpreima  5618  respreima  5621  dffo3  5640  dffo5  5642  f1ompt  5644  ffnfvf  5652  fmptco  5659  ftpg  5677  fnressn  5679  idref  5733  abrexco  5735  dff13  5744  dff13f  5746  fliftel  5769  isoini  5794  eusvobj2  5836  acexmidlema  5841  acexmidlemb  5842  acexmidlemph  5843  acexmidlem2  5847  oprabid  5882  brabvv  5896  dfoprab2  5897  eqoprab2b  5908  dmoprab  5931  rnoprab  5933  eloprabga  5937  mpomptx  5941  resoprab  5946  ffnov  5954  elrnmpo  5963  ralrnmpo  5964  rexrnmpo  5965  ovid  5966  ovi3  5986  ov6g  5987  foov  5996  opabex3d  6097  opabex3  6098  abexssex  6101  oprabex3  6105  oprabrexex2  6106  fmpo  6177  xporderlem  6207  f1od2  6211  mpoxopovel  6217  brtpos2  6227  dmtpos  6232  tpostpos  6240  tpossym  6252  tposoprab  6256  dfsmo2  6263  tfrlem7  6293  tfrlem9  6295  tfr1onlemaccex  6324  tfrcllemaccex  6337  tfrcldm  6339  frecabex  6374  el1o  6413  dif1o  6414  dfer2  6510  brdifun  6536  eqerlem  6540  qsid  6574  iinerm  6581  riinerm  6582  erinxp  6583  brecop  6599  eroveu  6600  erovlem  6601  ecopovsym  6605  mapval2  6652  mapsn  6664  elixp  6679  ixpeq2  6686  ixpin  6697  ixpiinm  6698  mptelixpg  6708  ixpsnf1o  6710  domen  6725  isfi  6735  en1  6773  xpsnen  6795  xpcomco  6800  xpassen  6804  ssenen  6825  nneneq  6831  snnen2oprc  6834  ac6sfi  6872  exmidpw  6882  exmidpweq  6883  pw1dc1  6887  eldju  7041  djur  7042  eldju2ndl  7045  eldju2ndr  7046  finomni  7112  acfun  7171  pw1nel3  7195  sucpw1nel3  7197  ccfunen  7213  elni  7257  ltexpi  7286  enq0enq  7380  enq0ref  7382  enq0tr  7383  prarloclem3  7446  ltdfpr  7455  genpdflem  7456  genpassl  7473  genpassu  7474  nqprrnd  7492  nqprl  7500  nqpru  7501  ltexprlemopl  7550  ltexprlemopu  7552  ltexprlemdisj  7555  ltexprlemloc  7556  recexprlemdisj  7579  caucvgprprlemell  7634  caucvgprprlemelu  7635  suplocexprlemml  7665  suplocsrlemb  7755  opelcn  7775  elreal  7777  elreal2  7779  peano1nnnn  7801  axicn  7812  axaddf  7817  axmulf  7818  axprecex  7829  axpre-ltirr  7831  axpre-mulgt0  7836  axcaucvglemres  7848  axpre-suploc  7851  xrlenlt  7971  ltxrlt  7972  inelr  8490  reapcotr  8504  1nn  8876  elnnne0  9136  un0addcl  9155  un0mulcl  9156  elnnz  9209  elznn0nn  9213  elznn0  9214  elznn  9215  elz2  9270  zapne  9273  3halfnz  9296  prime  9298  raluz2  9525  rexuz2  9527  supinfneg  9541  infsupneg  9542  eluz2b2  9549  eluz2b3  9550  ublbneg  9559  elq  9568  qreccl  9588  elpq  9594  ralrp  9619  rexrp  9620  rpnegap  9630  ltxr  9719  xrnemnf  9721  xrltso  9740  icc0r  9870  divelunit  9946  fzprval  10025  fztpval  10026  elfz1b  10033  fz01or  10054  4fvwrd4  10083  fzolb  10096  fzolb2  10097  elfzo3  10106  fzouzsplit  10122  elfzo0z  10127  fzo0m  10134  fzind2  10182  ioo0  10203  ico0  10205  ioc0  10206  uzennn  10379  seq3f1olemp  10445  caucvgre  10932  cvg1nlemcau  10935  resqrexlemex  10976  climeu  11246  fsum2dlemstep  11384  expcnv  11454  prodsnf  11542  fprod2dlemstep  11572  divides  11738  m1exp1  11847  divalgb  11871  bezoutlemnewy  11938  bezoutlemmain  11940  bezoutlemex  11943  dfgcd2  11956  nnwosdc  11981  lcmgcdlem  12018  isprm2  12058  isprm3  12059  isprm4  12060  isprm5  12083  sqrt2irr  12103  oddpwdc  12115  pythagtriplem19  12223  pythagtrip  12224  pceu  12236  dvdsprmpweqnn  12276  4sqlem2  12328  ennnfoneleminc  12353  ennnfonelemex  12356  ennnfonelemr  12365  ctiunct  12382  infpn2  12398  ismnd  12642  dfgrp2e  12720  istps  12783  istps2  12784  isbasis2g  12796  tgval2  12804  txuni2  13009  tx1cn  13022  tx2cn  13023  uptx  13027  txdis1cn  13031  blres  13187  xmeterval  13188  xmeter  13189  isxms2  13205  isms2  13207  metrest  13259  qtopbasss  13274  dedekindicclemicc  13363  limcdifap  13384  pilem1  13453  sincosq1lem  13499  2sqlem1  13703  decidr  13790  bdcuni  13871  bdcriota  13878  bdinex1  13894  bj-zfpair2  13905  bj-axun2  13910  bj-ssom  13931  ss1oel2o  13986  nninfsellemdc  14003  nninfsellemsuc  14005  nninfsellemqall  14008  trirec0xor  14037  iswomni0  14043