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  938  orbididc  942  pm5.75  951  3orass  970  3anass  971  3ancomb  975  3anan32  978  3anan12  979  anandi3  980  anandi3r  981  xordc  1381  falbitru  1406  19.26-2  1469  19.26-3an  1470  alrot3  1472  albiim  1474  2albiim  1475  19.27h  1547  19.27  1548  19.28h  1549  19.28  1550  nfalt  1565  aaanh  1573  aaan  1574  alinexa  1590  19.21-2  1654  nf2  1655  19.44  1669  19.45  1670  exrot3  1677  exrot4  1678  eeor  1682  sbcof2  1797  sbid2h  1836  19.23vv  1871  sbnv  1875  sblimv  1881  pm11.53  1882  19.41vv  1890  19.41vvv  1891  19.41vvvv  1892  exdistrv  1897  19.42vv  1898  19.42vvv  1899  19.42vvvv  1900  4exdistr  1903  cbvex4v  1917  eean  1918  sbn  1939  sbim  1940  sbor  1941  sban  1942  sbrim  1943  sblim  1944  sbbi  1946  sblbis  1947  sbrbis  1948  sbrbif  1949  sbco2d  1953  sbco2vd  1954  sbnf2  1968  2sb5  1970  2sb6  1971  sbcom2v  1972  sbcom2v2  1973  sbcom2  1974  sb6a  1975  2sb5rf  1976  2sb6rf  1977  sbalyz  1986  sbal  1987  sbal1yz  1988  sbex  1991  sbalv  1992  sbco4lem  1993  exsb  1995  2exsb  1996  eujust  2015  euf  2018  cbveu  2037  mor  2055  eu2  2057  mo4f  2073  eu4  2075  2exeu  2105  2eu4  2106  exists1  2109  abid  2152  eleq12i  2232  abeq2  2273  abeq2i  2275  clabel  2291  abid2f  2332  sbabel  2333  neeq12i  2351  neanior  2421  ralnex  2452  dfrex2dc  2455  ralinexa  2491  nfraldya  2499  nfrexdya  2500  r3al  2508  r19.26-2  2593  ralbiim  2598  ralnex2  2603  r19.43  2622  ralcomf  2625  rexcomf  2626  rexrot4  2630  reean  2632  3reeanv  2634  rabbi  2641  cbvralf  2682  cbvrexf  2683  cbvreu  2687  cbvral2v  2700  cbvrex2v  2701  cbvral3v  2702  cbvralsv  2703  cbvrexsv  2704  sbralie  2705  rabeq2i  2718  issetf  2728  2gencl  2754  3gencl  2755  ceqsex2  2761  ceqsex3v  2763  ceqsex6v  2765  ceqsex8v  2766  gencbvex  2767  gencbval  2769  spc2gv  2812  eqvincf  2846  ceqsrex2v  2853  clel5  2858  elrab2  2880  ralab  2881  ralrab  2882  rexab  2883  rexrab  2884  ralab2  2885  rexab2  2887  eueq3dc  2895  morex  2905  euind  2908  reu2  2909  reu6  2910  rmo4  2914  reu4  2915  reu7  2916  rmo3f  2918  rmo4f  2919  rmoim  2922  2reuswapdc  2925  reuind  2926  2rmorex  2927  sbcco  2967  sbccomlem  3020  sbccom  3021  ra5  3034  rmo3  3037  csbco  3050  csbcow  3051  sbnfc2  3100  csbabg  3101  cbvralcsf  3102  cbvrexcsf  3103  cbvreucsf  3104  dfss  3125  dfss2f  3128  ss2ab  3205  dfdif3  3227  difeqri  3237  ddifstab  3249  raldifb  3257  uneqri  3259  ssequn2  3290  unss  3291  rexun  3297  ralunb  3298  elin2  3305  ineqri  3310  dfss1  3321  dfss5  3322  dfss4st  3350  ssddif  3351  difin  3354  indif  3360  difundi  3369  indifdir  3373  symdifxor  3383  inrab2  3390  rabun2  3396  reuun2  3400  0el  3426  rabeq0  3433  abeq0  3434  disjr  3453  disj1  3454  undif4  3466  uneqdifeqim  3489  r19.2m  3490  r19.3rm  3492  r19.9rmv  3495  raaan  3510  pwss  3569  dfpr2  3589  rexdifpr  3598  ralsnsg  3607  ralsns  3608  eltpg  3615  eldiftp  3616  ralprg  3621  rexprg  3622  raltpg  3623  rextpg  3624  snprc  3635  rabrsndc  3638  euabsn2  3639  eusn  3644  eldifsn  3697  ssdifsn  3698  rexdifsn  3702  eqsnm  3729  tpss  3732  snsssn  3735  prel12  3745  preqsn  3749  oprcl  3776  pwtpss  3780  eluniab  3795  elunirab  3796  unipr  3797  dfnfc2  3801  uniun  3802  uniin  3803  uni0b  3808  unissb  3813  elintab  3829  elintrab  3830  ssintab  3835  ssintrab  3841  intun  3849  intpr  3850  elrint  3858  iuncom4  3867  iuneq2  3876  dfiun2g  3892  ssiinf  3909  iundif2ss  3925  elriin  3930  iunxiun  3941  pwssb  3945  elpwpw  3946  iunpwss  3951  dfdisj2  3955  disjiun  3971  cbvopab1  4049  dftr5  4077  trint  4089  inex1  4110  inuni  4128  repizf2lem  4134  unidif0  4140  axpweq  4144  bnd2  4146  exmid01  4171  zfpair2  4182  exss  4199  elop  4203  opm  4206  otth  4214  copsex4g  4219  opeqsn  4224  opelopabsbALT  4231  brabga  4236  opelopabaf  4245  iunopab  4253  pwunss  4255  pocl  4275  frirrg  4322  elsuci  4375  elsucg  4376  sucel  4382  unisucg  4386  uniuni  4423  reusv3  4432  iunpw  4452  setindel  4509  elirr  4512  en2lp  4525  ordpwsucss  4538  zfregfr  4545  tfi  4553  peano2  4566  peano5  4569  elxp  4615  opelxp  4628  brxp  4629  rabxp  4635  opthprc  4649  brab2a  4651  opeliunxp  4653  xpundi  4654  xpundir  4655  elvvv  4661  brinxp  4666  brab2ga  4673  0xp  4678  ssrel2  4688  eqrelrel  4699  reliun  4719  reluni  4721  raliunxp  4739  rexiunxp  4740  ralxpf  4744  rexxpf  4745  iunxpf  4746  relop  4748  elco  4764  elcnv  4775  elcnv2  4776  dmin  4806  dmuni  4808  dmopab  4809  dmi  4813  dmmrnm  4817  rnopab  4845  elrnmpt1  4849  rncoeq  4871  resiexg  4923  dfima2  4942  dfima3  4943  elima2  4946  elima3  4947  imai  4954  elimasn  4965  epini  4969  dfse2  4971  cotr  4979  issref  4980  intasym  4982  asymref  4983  cnvopab  4999  cnvi  5002  cnvdif  5004  imainss  5013  rnxpid  5032  dfrel2  5048  dfrel3  5055  dmsnm  5063  rnsnm  5064  relsn2m  5068  dmsnopg  5069  cnvcnvsn  5074  elxp4  5085  elxp5  5086  cnvresima  5087  mptpreima  5091  dfco2  5097  coundi  5099  coundir  5100  imaco  5103  coiun  5107  coi1  5113  relssdmrn  5118  relrelss  5124  unixpm  5133  ressn  5138  cnviinm  5139  cnvpom  5140  cnvsom  5141  cbviota  5152  iotass  5164  dffun2  5192  dffun4  5193  dffun7  5209  dffun8  5210  dffun9  5211  funopab  5217  funun  5226  funcnvsn  5227  fntpg  5238  funcnv2  5242  funcnv  5243  fun2cnv  5246  fncnv  5248  fun11  5249  fununi  5250  imadiflem  5261  imadif  5262  imainlem  5263  funimaexglem  5265  fnunsn  5289  fnres  5298  fnopabg  5305  mptfng  5307  mptun  5313  fun  5354  fcnvres  5365  dff12  5386  f1cnvcnv  5398  funforn  5411  dff1o2  5431  dff1o5  5435  f1orn  5436  resdif  5448  ffoss  5458  f11o  5459  f1o00  5461  fo00  5462  elfv  5478  fv3  5503  nfvres  5513  eqfnfv3  5579  fneqeql  5587  unpreima  5604  respreima  5607  dffo3  5626  dffo5  5628  f1ompt  5630  ffnfvf  5638  fmptco  5645  ftpg  5663  fnressn  5665  idref  5719  abrexco  5721  dff13  5730  dff13f  5732  fliftel  5755  isoini  5780  eusvobj2  5822  acexmidlema  5827  acexmidlemb  5828  acexmidlemph  5829  acexmidlem2  5833  oprabid  5865  brabvv  5879  dfoprab2  5880  eqoprab2b  5891  dmoprab  5914  rnoprab  5916  eloprabga  5920  mpomptx  5924  resoprab  5929  ffnov  5937  elrnmpo  5946  ralrnmpo  5947  rexrnmpo  5948  ovid  5949  ovi3  5969  ov6g  5970  foov  5979  opabex3d  6081  opabex3  6082  abexssex  6085  oprabex3  6089  oprabrexex2  6090  fmpo  6161  xporderlem  6190  f1od2  6194  mpoxopovel  6200  brtpos2  6210  dmtpos  6215  tpostpos  6223  tpossym  6235  tposoprab  6239  dfsmo2  6246  tfrlem7  6276  tfrlem9  6278  tfr1onlemaccex  6307  tfrcllemaccex  6320  tfrcldm  6322  frecabex  6357  el1o  6396  dif1o  6397  dfer2  6493  brdifun  6519  eqerlem  6523  qsid  6557  iinerm  6564  riinerm  6565  erinxp  6566  brecop  6582  eroveu  6583  erovlem  6584  ecopovsym  6588  mapval2  6635  mapsn  6647  elixp  6662  ixpeq2  6669  ixpin  6680  ixpiinm  6681  mptelixpg  6691  ixpsnf1o  6693  domen  6708  isfi  6718  en1  6756  xpsnen  6778  xpcomco  6783  xpassen  6787  ssenen  6808  nneneq  6814  snnen2oprc  6817  ac6sfi  6855  exmidpw  6865  exmidpweq  6866  pw1dc1  6870  eldju  7024  djur  7025  eldju2ndl  7028  eldju2ndr  7029  finomni  7095  acfun  7154  pw1nel3  7178  sucpw1nel3  7180  ccfunen  7196  elni  7240  ltexpi  7269  enq0enq  7363  enq0ref  7365  enq0tr  7366  prarloclem3  7429  ltdfpr  7438  genpdflem  7439  genpassl  7456  genpassu  7457  nqprrnd  7475  nqprl  7483  nqpru  7484  ltexprlemopl  7533  ltexprlemopu  7535  ltexprlemdisj  7538  ltexprlemloc  7539  recexprlemdisj  7562  caucvgprprlemell  7617  caucvgprprlemelu  7618  suplocexprlemml  7648  suplocsrlemb  7738  opelcn  7758  elreal  7760  elreal2  7762  peano1nnnn  7784  axicn  7795  axaddf  7800  axmulf  7801  axprecex  7812  axpre-ltirr  7814  axpre-mulgt0  7819  axcaucvglemres  7831  axpre-suploc  7834  xrlenlt  7954  ltxrlt  7955  inelr  8473  reapcotr  8487  1nn  8859  elnnne0  9119  un0addcl  9138  un0mulcl  9139  elnnz  9192  elznn0nn  9196  elznn0  9197  elznn  9198  elz2  9253  zapne  9256  3halfnz  9279  prime  9281  raluz2  9508  rexuz2  9510  supinfneg  9524  infsupneg  9525  eluz2b2  9532  eluz2b3  9533  ublbneg  9542  elq  9551  qreccl  9571  elpq  9577  ralrp  9602  rexrp  9603  rpnegap  9613  ltxr  9702  xrnemnf  9704  xrltso  9723  icc0r  9853  divelunit  9929  fzprval  10007  fztpval  10008  elfz1b  10015  fz01or  10036  4fvwrd4  10065  fzolb  10078  fzolb2  10079  elfzo3  10088  fzouzsplit  10104  elfzo0z  10109  fzo0m  10116  fzind2  10164  ioo0  10185  ico0  10187  ioc0  10188  uzennn  10361  seq3f1olemp  10427  caucvgre  10909  cvg1nlemcau  10912  resqrexlemex  10953  climeu  11223  fsum2dlemstep  11361  expcnv  11431  prodsnf  11519  fprod2dlemstep  11549  divides  11715  m1exp1  11823  divalgb  11847  bezoutlemnewy  11914  bezoutlemmain  11916  bezoutlemex  11919  dfgcd2  11932  lcmgcdlem  11988  isprm2  12028  isprm3  12029  isprm4  12030  sqrt2irr  12071  oddpwdc  12083  pythagtriplem19  12191  pythagtrip  12192  pceu  12204  dvdsprmpweqnn  12244  ennnfoneleminc  12281  ennnfonelemex  12284  ennnfonelemr  12293  ctiunct  12310  istps  12571  istps2  12572  isbasis2g  12584  tgval2  12592  txuni2  12797  tx1cn  12810  tx2cn  12811  uptx  12815  txdis1cn  12819  blres  12975  xmeterval  12976  xmeter  12977  isxms2  12993  isms2  12995  metrest  13047  qtopbasss  13062  dedekindicclemicc  13151  limcdifap  13172  pilem1  13241  sincosq1lem  13287  decidr  13512  bdcuni  13593  bdcriota  13600  bdinex1  13616  bj-zfpair2  13627  bj-axun2  13632  bj-ssom  13653  ss1oel2o  13707  nninfsellemdc  13724  nninfsellemsuc  13726  nninfsellemqall  13729  trirec0xor  13758  iswomni0  13764