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  4205  dftr5  4234  trint  4246  inex1  4269  inuni  4293  repizf2lem  4300  unidif0  4306  axpweq  4310  bnd2  4312  exmid01  4337  zfpair2  4349  exss  4369  elop  4373  opm  4376  otth  4384  copsex4g  4389  opeqsn  4395  opelopabsbALT  4403  brabga  4408  opelopabaf  4418  iunopab  4426  pwunss  4430  pocl  4450  frirrg  4497  elsuci  4550  elsucg  4551  sucel  4557  unisucg  4561  uniuni  4599  reusv3  4608  iunpw  4628  setindel  4687  elirr  4690  en2lp  4703  ordpwsucss  4716  zfregfr  4723  tfi  4731  peano2  4744  peano5  4747  elxp  4793  opelxp  4806  brxp  4807  rabxp  4814  opthprc  4828  brab2a  4830  opeliunxp  4832  xpundi  4833  xpundir  4834  elvvv  4840  brinxp  4845  brab2ga  4852  0xp  4857  ssrel2  4867  eqrelrel  4878  reliun  4900  reluni  4902  raliunxp  4923  rexiunxp  4924  ralxpf  4928  rexxpf  4929  iunxpf  4930  relop  4932  elco  4948  elcnv  4959  elcnv2  4960  dmin  4991  dmuni  4993  dmopab  4994  dmi  4998  dmmrnm  5003  rnopab  5031  elrnmpt1  5035  rncoeq  5058  resiexg  5111  restidsing  5122  dfima2  5131  dfima3  5132  elima2  5135  elima3  5136  imai  5146  elimasn  5157  epini  5161  dfse2  5163  cotr  5172  issref  5173  intasym  5175  asymref  5176  cnvopab  5192  cnvi  5195  cnvdif  5197  imainss  5206  rnxpid  5225  dfrel2  5241  dfrel3  5248  dmsnm  5256  rnsnm  5257  relsn2m  5261  dmsnopg  5262  cnvcnvsn  5267  elxp4  5278  elxp5  5279  cnvresima  5280  mptpreima  5284  dfco2  5290  coundi  5292  coundir  5293  imaco  5296  coiun  5300  coi1  5306  relssdmrn  5311  relrelss  5317  unixpm  5326  ressn  5331  cnviinm  5332  cnvpom  5333  cnvsom  5334  cbviota  5345  iotass  5358  eliota  5368  dffun2  5390  dffun4  5391  dffun7  5407  dffun8  5408  dffun9  5409  funopab  5415  funun  5425  funcnvsn  5429  fntpg  5440  funcnv2  5444  funcnv  5445  fun2cnv  5448  fncnv  5450  fun11  5451  fununi  5452  imadiflem  5463  imadif  5464  imainlem  5465  funimaexglem  5467  fnunsn  5493  fnres  5503  fnopabg  5510  mptfng  5512  mptun  5518  fun  5564  fcnvres  5578  dff12  5600  f1cnvcnv  5612  funforn  5625  dff1o2  5647  dff1o5  5651  f1orn  5652  resdif  5664  ffoss  5675  f11o  5676  f1o00  5679  fo00  5680  elfv  5696  fv3  5721  nfvres  5735  eqfnfv3  5811  fneqeql  5820  unpreima  5836  respreima  5839  dffo3  5858  dffo5  5860  f1ompt  5862  ffnfvf  5870  fmptco  5877  funopdmsn  5898  ftpg  5902  fnressn  5904  idref  5965  abrexco  5968  dff13  5977  dff13f  5979  fliftel  6002  isoini  6027  eusvobj2  6074  acexmidlema  6079  acexmidlemb  6080  acexmidlemph  6081  acexmidlem2  6085  oprabid  6120  brabvv  6137  dfoprab2  6138  eqoprab2b  6149  dmoprab  6172  rnoprab  6174  eloprabga  6178  mpomptx  6182  resoprab  6187  ffnov  6195  elrnmpo  6205  ralrnmpo  6206  rexrnmpo  6207  ovid  6208  ovi3  6229  ov6g  6230  foov  6239  opabex3d  6354  opabex3  6355  abexssex  6358  oprabex3  6366  oprabrexex2  6367  fmpo  6441  xporderlem  6471  f1od2  6475  mpoxopovel  6516  brtpos2  6526  dmtpos  6531  tpostpos  6539  tpossym  6551  tposoprab  6555  dfsmo2  6562  tfrlem7  6592  tfrlem9  6594  tfr1onlemaccex  6623  tfrcllemaccex  6636  tfrcldm  6638  frecabex  6673  el1o  6714  dif1o  6715  dfer2  6812  brdifun  6838  eqerlem  6842  qsid  6878  iinerm  6885  riinerm  6886  erinxp  6887  brecop  6903  eroveu  6904  erovlem  6905  ecopovsym  6909  mapval2  6963  mapsn  6977  elixp  6992  ixpeq2  6999  ixpin  7010  ixpiinm  7011  mptelixpg  7021  ixpsnf1o  7023  domen  7040  isfi  7052  en1  7091  modom2  7114  xpsnen  7124  xpcomco  7129  xpassen  7133  ssenen  7157  nneneq  7163  snnen2oprc  7166  ac6sfi  7207  exmidpw  7220  exmidpweq  7221  pw1dc1  7226  elfpw  7267  eldju  7415  djur  7416  eldju2ndl  7419  eldju2ndr  7420  finomni  7487  nninfwlporlemd  7519  nninfwlpoimlemg  7522  acfun  7570  pw1nel3  7597  sucpw1nel3  7599  ccfunen  7637  elni  7682  ltexpi  7711  enq0enq  7805  enq0ref  7807  enq0tr  7808  prarloclem3  7871  ltdfpr  7880  genpdflem  7881  genpassl  7898  genpassu  7899  nqprrnd  7917  nqprl  7925  nqpru  7926  ltexprlemopl  7975  ltexprlemopu  7977  ltexprlemdisj  7980  ltexprlemloc  7981  recexprlemdisj  8004  caucvgprprlemell  8059  caucvgprprlemelu  8060  suplocexprlemml  8090  suplocsrlemb  8180  opelcn  8200  elreal  8202  elreal2  8204  peano1nnnn  8226  axicn  8237  axaddf  8242  axmulf  8243  axprecex  8254  axpre-ltirr  8256  axpre-mulgt0  8261  axcaucvglemres  8273  axpre-suploc  8276  xrlenlt  8397  ltxrlt  8398  inelr  8921  reapcotr  8935  1nn  9325  elnnne0  9589  un0addcl  9608  un0mulcl  9609  elnnz  9666  elznn0nn  9670  elznn0  9671  elznn  9672  elz2  9728  zapne  9731  3halfnz  9755  prime  9757  raluz2  9996  rexuz2  9998  supinfneg  10012  infsupneg  10013  eluz2b2  10020  eluz2b3  10021  ublbneg  10030  elq  10039  qreccl  10059  elpq  10067  ralrp  10094  rexrp  10095  rpnegap  10105  ltxr  10195  xrnemnf  10197  xrltso  10216  icc0r  10346  divelunit  10422  fzprval  10507  fztpval  10508  elfz1b  10515  fz01or  10536  4fvwrd4  10565  fzolb  10579  fzolb2  10580  elfzo3  10589  fzouzsplit  10606  elfzo0z  10614  fzo0m  10622  fzind2  10676  infssfzcldc  10687  infssfzledc  10688  ioo0  10712  ico0  10714  ioc0  10715  uzennn  10895  seq3f1olemp  10974  sseqn  11302  hashfibc  11306  hashf1lem2  11309  iswrd  11329  caucvgre  11770  cvg1nlemcau  11773  resqrexlemex  11814  climeu  12088  fsum2dlemstep  12227  expcnv  12297  prodsnf  12385  fprod2dlemstep  12415  divides  12582  m1exp1  12694  divalgb  12718  bitsval2  12737  bitsmod  12749  bitscmp  12751  bezoutlemnewy  12799  bezoutlemmain  12801  bezoutlemex  12804  dfgcd2  12817  nnwosdc  12842  lcmgcdlem  12881  isprm2  12921  isprm3  12922  isprm4  12923  isprm5  12947  sqrt2irr  12967  pythagtriplem19  13091  pythagtrip  13092  pceu  13104  dvdsprmpweqnn  13145  4sqlem2  13198  4sqlem12  13211  dec5dvds2  13222  ballotfilemodife  13299  ballotfilem4  13300  ennnfoneleminc  13361  ennnfonelemex  13364  ennnfonelemr  13373  ctiunct  13390  infpn2  13406  xpsfrnel  13725  xpsfrnel2  13727  gzsum0  13773  ismnd  13792  dfgrp2e  13893  dfgrp3me  13965  isnsg2  14066  eqger  14087  elcntr  14164  cntzrec  14170  isabl2  14188  imasabl  14231  idjusnfi  14271  gsum2d2fi  14275  isrhm  14575  isrim  14586  isnzr2  14601  drngprop  14727  lss1d  14830  istps  15270  istps2  15271  isbasis2g  15283  tgval2  15289  txuni2  15494  tx1cn  15507  tx2cn  15508  uptx  15512  txdis1cn  15516  blres  15672  xmeterval  15673  xmeter  15674  isxms2  15690  isms2  15692  metrest  15744  qtopbasss  15759  dedekindicclemicc  15870  limcdifap  15900  plyrecj  16001  pilem1  16018  sincosq1lem  16064  mpodvdsmulf1o  16296  gausslemma2dlem1a  16394  gausslemma2dlem4  16400  lgsquadlem1  16413  lgsquadlem2  16414  2lgslem1b  16425  2sqlem1  16450  upgrex  16561  griedg0ssusgr  16709  clwwlkn1loopb  16878  clwwlknon2x  16893  decidr  17041  bdcuni  17119  bdcriota  17126  bdinex1  17142  bj-zfpair2  17153  bj-axun2  17158  bj-ssom  17179  ss1oel2o  17234  idjudju  17264  nninfsellemdc  17271  nninfsellemsuc  17273  nninfsellemqall  17276  trirec0xor  17313  iswomni0  17320  alsralrex  17372  alsraln0m  17373  2alsraln0m  17377  2alsraln0idm  17378  dfalseu2  17396