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 ⊢ (𝜑 ↔ 𝜒)

This proof depends on syntax axioms:   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bitr2i  185  bitr3i  186  bitr4i  187  bitrd  188  3bitri  206  3bitr2i  208  3bitr3i  210  3bitr4i  212  bibi12i  229  imbi12i  239  pm4.71r  394  biadan2  460  anbi2ci  463  anbi12i  464  anbi12ci  465  bianassc  474  pm5.3  479  an42  593  xchbinx  693  mt2bi  695  orbi12i  776  or42  784  pm5.53  814  orddi  832  anddi  833  pm2.1dc  849  dcim  853  notnotrdc  855  dcnnOLD  861  rbaib  933  rbaibr  934  pm4.43  962  orbididc  966  pm5.75  975  ifptru  1002  ifpfal  1003  3orass  1012  3anass  1013  3ancomb  1017  3anan32  1020  3anan12  1021  anandi3  1022  anandi3r  1023  xordc  1441  falbitru  1466  19.26-2  1535  19.26-3an  1536  alrot3  1538  albiim  1540  2albiim  1541  19.27h  1613  19.27  1614  19.28h  1615  19.28  1616  nfalt  1631  aaanh  1639  aaan  1640  alinexa  1656  19.21-2  1719  nf2  1720  19.44  1734  19.45  1735  exrot3  1742  exrot4  1743  eeor  1747  sbcof2  1863  sbid2h  1902  19.23vv  1937  sbnv  1943  sblimv  1950  pm11.53  1951  19.41vv  1959  19.41vvv  1960  19.41vvvv  1961  exdistrv  1966  19.42vv  1967  19.42vvv  1968  19.42vvvv  1969  4exdistr  1972  cbvex4v  1990  eean  1991  sbn  2012  sbim  2013  sbor  2014  sban  2015  sbrim  2016  sblim  2017  sbbi  2019  sblbis  2020  sbrbis  2021  sbrbif  2022  sbco2d  2026  sbco2vd  2027  sbnf2  2041  2sb5  2043  2sb6  2044  sbcom2v  2045  sbcom2v2  2046  sbcom2  2047  sb6a  2048  2sb5rf  2049  2sb6rf  2050  sbalyz  2059  sbal  2060  sbal1yz  2061  sbex  2064  sbalv  2065  sbco4lem  2066  exsb  2068  2exsb  2069  eujust  2088  euf  2091  cbveu  2110  mor  2129  eu2  2131  mo4f  2147  eu4  2149  2exeu  2179  2eu4  2180  exists1  2183  abid  2226  eleq12i  2306  abeq2  2347  abeq2i  2349  abbib  2356  clabel  2367  eqabb  2374  eqabbw  2375  abid2f  2418  sbabel  2419  neeq12i  2437  neanior  2507  ralnex  2538  dfrex2dc  2541  ralinexa  2577  nfraldya  2585  nfrexdya  2586  r3al  2594  r19.26-2  2680  ralbiim  2685  ralnex2  2690  r19.43  2709  ralcomf  2712  rexcomf  2713  ralrot3  2716  rexrot4  2718  reean  2720  3reeanv  2722  reqabi  2728  rabbi  2730  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvral2vw  2797  cbvrex2vw  2798  cbvral2v  2799  cbvrex2v  2800  cbvral3v  2801  cbvralsv  2802  cbvrexsv  2803  sbralie  2804  rabeq2i  2818  issetf  2829  2gencl  2855  3gencl  2856  ceqsex2  2863  ceqsex3v  2865  ceqsex6v  2867  ceqsex8v  2868  gencbvex  2869  gencbval  2871  spc2gv  2916  eqvincf  2951  ceqsrex2v  2958  clel5  2963  elrab2  2985  ralab  2986  ralrab  2987  rexab  2988  rexrab  2989  ralab2  2990  rexab2  2992  eueq3dc  3000  morex  3010  euind  3013  reu2  3014  reu6  3015  rmo4  3019  reu4  3020  reu7  3021  rmo3f  3023  rmo4f  3024  rmoim  3027  2reuswapdc  3030  reuind  3031  2rmorex  3032  sbcco  3073  sbccomlem  3126  sbccom  3127  ra5  3141  rmo3  3144  csbco  3157  csbcow  3158  sbnfc2  3208  csbabg  3209  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  dfss  3234  dfssf  3238  dfss2f  3239  ss2ab  3316  dfdif3  3339  difeqri  3349  ddifstab  3361  raldifb  3369  uneqri  3371  ssequn2  3402  unss  3403  rexun  3409  ralunb  3410  elin2  3417  ineqri  3424  dfss1  3435  dfss5  3436  dfss4st  3464  ssddif  3465  difin  3468  indif  3474  difundi  3483  indifdir  3487  symdifxor  3497  inrab2  3506  rabun2  3512  reuun2  3516  0el  3544  ab0w  3550  rabeq0  3552  abeq0  3553  disjr  3574  disj1  3575  undif4  3587  uneqdifeqim  3613  r19.2m  3614  r19.3rm  3616  r19.9rmv  3619  raaan  3633  pwss  3708  dfpr2  3728  rexdifpr  3737  ralsnsg  3746  ralsns  3747  eltpg  3754  eldiftp  3755  ralprg  3760  rexprg  3761  raltpg  3762  rextpg  3763  snprc  3774  rabrsndc  3779  euabsn2  3780  eusn  3785  eldifsn  3841  ssdifsn  3842  rexdifsn  3846  eqsnm  3880  tpss  3883  snsssn  3886  prel12  3896  preqsn  3900  oprcl  3928  pwtpss  3932  eluniab  3947  elunirab  3948  unipr  3949  dfnfc2  3953  uniun  3954  uniin  3955  uni0b  3960  unissb  3965  elintab  3981  elintrab  3982  ssintab  3987  ssintrab  3993  intun  4001  intpr  4002  elrint  4010  iuncom4  4019  iuneq2  4028  dfiun2g  4044  ssiinf  4062  iundif2ss  4078  elriin  4083  iunxiun  4094  pwssb  4098  elpwpw  4099  iunpwss  4104  dfdisj2  4108  disjiun  4125  cbvopab1  4204  dftr5  4232  trint  4244  inex1  4267  inuni  4291  repizf2lem  4298  unidif0  4304  axpweq  4308  bnd2  4310  exmid01  4335  zfpair2  4347  exss  4367  elop  4371  opm  4374  otth  4382  copsex4g  4387  opeqsn  4393  opelopabsbALT  4401  brabga  4406  opelopabaf  4416  iunopab  4424  pwunss  4428  pocl  4448  frirrg  4495  elsuci  4548  elsucg  4549  sucel  4555  unisucg  4559  uniuni  4597  reusv3  4606  iunpw  4626  setindel  4685  elirr  4688  en2lp  4701  ordpwsucss  4714  zfregfr  4721  tfi  4729  peano2  4742  peano5  4745  elxp  4791  opelxp  4804  brxp  4805  rabxp  4812  opthprc  4826  brab2a  4828  opeliunxp  4830  xpundi  4831  xpundir  4832  elvvv  4838  brinxp  4843  brab2ga  4850  0xp  4855  ssrel2  4865  eqrelrel  4876  reliun  4898  reluni  4900  raliunxp  4921  rexiunxp  4922  ralxpf  4926  rexxpf  4927  iunxpf  4928  relop  4930  elco  4946  elcnv  4957  elcnv2  4958  dmin  4989  dmuni  4991  dmopab  4992  dmi  4996  dmmrnm  5001  rnopab  5029  elrnmpt1  5033  rncoeq  5056  resiexg  5108  restidsing  5119  dfima2  5128  dfima3  5129  elima2  5132  elima3  5133  imai  5143  elimasn  5154  epini  5158  dfse2  5160  cotr  5169  issref  5170  intasym  5172  asymref  5173  cnvopab  5189  cnvi  5192  cnvdif  5194  imainss  5203  rnxpid  5222  dfrel2  5238  dfrel3  5245  dmsnm  5253  rnsnm  5254  relsn2m  5258  dmsnopg  5259  cnvcnvsn  5264  elxp4  5275  elxp5  5276  cnvresima  5277  mptpreima  5281  dfco2  5287  coundi  5289  coundir  5290  imaco  5293  coiun  5297  coi1  5303  relssdmrn  5308  relrelss  5314  unixpm  5323  ressn  5328  cnviinm  5329  cnvpom  5330  cnvsom  5331  cbviota  5342  iotass  5355  eliota  5365  dffun2  5387  dffun4  5388  dffun7  5404  dffun8  5405  dffun9  5406  funopab  5412  funun  5422  funcnvsn  5426  fntpg  5437  funcnv2  5441  funcnv  5442  fun2cnv  5445  fncnv  5447  fun11  5448  fununi  5449  imadiflem  5460  imadif  5461  imainlem  5462  funimaexglem  5464  fnunsn  5490  fnres  5500  fnopabg  5507  mptfng  5509  mptun  5515  fun  5561  fcnvres  5575  dff12  5597  f1cnvcnv  5609  funforn  5622  dff1o2  5644  dff1o5  5648  f1orn  5649  resdif  5661  ffoss  5672  f11o  5673  f1o00  5676  fo00  5677  elfv  5693  fv3  5718  nfvres  5732  eqfnfv3  5808  fneqeql  5817  unpreima  5833  respreima  5836  dffo3  5855  dffo5  5857  f1ompt  5859  ffnfvf  5867  fmptco  5874  funopdmsn  5895  ftpg  5899  fnressn  5901  idref  5962  abrexco  5965  dff13  5974  dff13f  5976  fliftel  5999  isoini  6024  eusvobj2  6071  acexmidlema  6076  acexmidlemb  6077  acexmidlemph  6078  acexmidlem2  6082  oprabid  6117  brabvv  6134  dfoprab2  6135  eqoprab2b  6146  dmoprab  6169  rnoprab  6171  eloprabga  6175  mpomptx  6179  resoprab  6184  ffnov  6192  elrnmpo  6202  ralrnmpo  6203  rexrnmpo  6204  ovid  6205  ovi3  6226  ov6g  6227  foov  6236  opabex3d  6350  opabex3  6351  abexssex  6354  oprabex3  6362  oprabrexex2  6363  fmpo  6437  xporderlem  6467  f1od2  6471  mpoxopovel  6512  brtpos2  6522  dmtpos  6527  tpostpos  6535  tpossym  6547  tposoprab  6551  dfsmo2  6558  tfrlem7  6588  tfrlem9  6590  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfrcldm  6634  frecabex  6669  el1o  6710  dif1o  6711  dfer2  6808  brdifun  6834  eqerlem  6838  qsid  6874  iinerm  6881  riinerm  6882  erinxp  6883  brecop  6899  eroveu  6900  erovlem  6901  ecopovsym  6905  mapval2  6959  mapsn  6972  elixp  6987  ixpeq2  6994  ixpin  7005  ixpiinm  7006  mptelixpg  7016  ixpsnf1o  7018  domen  7035  isfi  7047  en1  7086  modom2  7109  xpsnen  7119  xpcomco  7124  xpassen  7128  ssenen  7152  nneneq  7158  snnen2oprc  7161  ac6sfi  7202  exmidpw  7215  exmidpweq  7216  pw1dc1  7221  elfpw  7262  eldju  7408  djur  7409  eldju2ndl  7412  eldju2ndr  7413  finomni  7480  nninfwlporlemd  7512  nninfwlpoimlemg  7515  acfun  7563  pw1nel3  7590  sucpw1nel3  7592  ccfunen  7630  elni  7675  ltexpi  7704  enq0enq  7798  enq0ref  7800  enq0tr  7801  prarloclem3  7864  ltdfpr  7873  genpdflem  7874  genpassl  7891  genpassu  7892  nqprrnd  7910  nqprl  7918  nqpru  7919  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemdisj  7973  ltexprlemloc  7974  recexprlemdisj  7997  caucvgprprlemell  8052  caucvgprprlemelu  8053  suplocexprlemml  8083  suplocsrlemb  8173  opelcn  8193  elreal  8195  elreal2  8197  peano1nnnn  8219  axicn  8230  axaddf  8235  axmulf  8236  axprecex  8247  axpre-ltirr  8249  axpre-mulgt0  8254  axcaucvglemres  8266  axpre-suploc  8269  xrlenlt  8390  ltxrlt  8391  inelr  8913  reapcotr  8927  1nn  9316  elnnne0  9579  un0addcl  9598  un0mulcl  9599  elnnz  9656  elznn0nn  9660  elznn0  9661  elznn  9662  elz2  9718  zapne  9721  3halfnz  9745  prime  9747  raluz2  9981  rexuz2  9983  supinfneg  9997  infsupneg  9998  eluz2b2  10005  eluz2b3  10006  ublbneg  10015  elq  10024  qreccl  10044  elpq  10051  ralrp  10078  rexrp  10079  rpnegap  10089  ltxr  10179  xrnemnf  10181  xrltso  10200  icc0r  10330  divelunit  10406  fzprval  10491  fztpval  10492  elfz1b  10499  fz01or  10520  4fvwrd4  10549  fzolb  10563  fzolb2  10564  elfzo3  10573  fzouzsplit  10590  elfzo0z  10598  fzo0m  10606  fzind2  10660  infssfzcldc  10671  infssfzledc  10672  ioo0  10696  ico0  10698  ioc0  10699  uzennn  10875  seq3f1olemp  10954  sseqn  11281  hashfibc  11285  hashf1lem2  11288  iswrd  11308  caucvgre  11749  cvg1nlemcau  11752  resqrexlemex  11793  climeu  12064  fsum2dlemstep  12203  expcnv  12273  prodsnf  12361  fprod2dlemstep  12391  divides  12558  m1exp1  12670  divalgb  12694  bitsval2  12713  bitsmod  12725  bitscmp  12727  bezoutlemnewy  12775  bezoutlemmain  12777  bezoutlemex  12780  dfgcd2  12793  nnwosdc  12818  lcmgcdlem  12857  isprm2  12897  isprm3  12898  isprm4  12899  isprm5  12922  sqrt2irr  12942  oddpwdc  12954  pythagtriplem19  13063  pythagtrip  13064  pceu  13076  dvdsprmpweqnn  13117  4sqlem2  13170  4sqlem12  13183  dec5dvds2  13194  ballotfilemodife  13242  ballotfilem4  13243  ennnfoneleminc  13304  ennnfonelemex  13307  ennnfonelemr  13316  ctiunct  13333  infpn2  13349  xpsfrnel  13667  xpsfrnel2  13669  gzsum0  13715  ismnd  13734  dfgrp2e  13835  dfgrp3me  13907  isnsg2  14008  eqger  14029  isabl2  14099  imasabl  14142  isrhm  14467  isrim  14478  isnzr2  14493  drngprop  14619  lss1d  14722  istps  15135  istps2  15136  isbasis2g  15148  tgval2  15154  txuni2  15359  tx1cn  15372  tx2cn  15373  uptx  15377  txdis1cn  15381  blres  15537  xmeterval  15538  xmeter  15539  isxms2  15555  isms2  15557  metrest  15609  qtopbasss  15624  dedekindicclemicc  15735  limcdifap  15765  plyrecj  15866  pilem1  15883  sincosq1lem  15929  mpodvdsmulf1o  16110  gausslemma2dlem1a  16189  gausslemma2dlem4  16195  lgsquadlem1  16208  lgsquadlem2  16209  2lgslem1b  16220  2sqlem1  16245  upgrex  16356  griedg0ssusgr  16504  clwwlkn1loopb  16673  clwwlknon2x  16688  decidr  16836  bdcuni  16914  bdcriota  16921  bdinex1  16937  bj-zfpair2  16948  bj-axun2  16953  bj-ssom  16974  ss1oel2o  17029  nninfsellemdc  17065  nninfsellemsuc  17067  nninfsellemqall  17070  trirec0xor  17106  iswomni0  17113  alsralrex  17165  alsraln0m  17166  2alsraln0m  17170  2alsraln0idm  17171  dfalseu2  17189