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

Syntax hints:   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bitr2i  185  bitr3i  186  bitr4i  187  bitrd  188  3bitri  206  3bitr2i  208  3bitr3i  210  3bitr4i  212  bibi12i  229  imbi12i  239  pm4.71r  390  biadan2  456  anbi2ci  459  anbi12i  460  anbi12ci  461  bianassc  470  pm5.3  475  an42  587  xchbinx  686  mt2bi  688  orbi12i  768  or42  776  pm5.53  806  orddi  824  anddi  825  pm2.1dc  841  dcim  845  notnotrdc  847  dcnnOLD  853  rbaib  925  rbaibr  926  pm4.43  954  orbididc  958  pm5.75  967  3orass  986  3anass  987  3ancomb  991  3anan32  994  3anan12  995  anandi3  996  anandi3r  997  xordc  1414  falbitru  1439  19.26-2  1508  19.26-3an  1509  alrot3  1511  albiim  1513  2albiim  1514  19.27h  1586  19.27  1587  19.28h  1588  19.28  1589  nfalt  1604  aaanh  1612  aaan  1613  alinexa  1629  19.21-2  1693  nf2  1694  19.44  1708  19.45  1709  exrot3  1716  exrot4  1717  eeor  1721  sbcof2  1836  sbid2h  1875  19.23vv  1910  sbnv  1915  sblimv  1921  pm11.53  1922  19.41vv  1930  19.41vvv  1931  19.41vvvv  1932  exdistrv  1937  19.42vv  1938  19.42vvv  1939  19.42vvvv  1940  4exdistr  1943  cbvex4v  1961  eean  1962  sbn  1983  sbim  1984  sbor  1985  sban  1986  sbrim  1987  sblim  1988  sbbi  1990  sblbis  1991  sbrbis  1992  sbrbif  1993  sbco2d  1997  sbco2vd  1998  sbnf2  2012  2sb5  2014  2sb6  2015  sbcom2v  2016  sbcom2v2  2017  sbcom2  2018  sb6a  2019  2sb5rf  2020  2sb6rf  2021  sbalyz  2030  sbal  2031  sbal1yz  2032  sbex  2035  sbalv  2036  sbco4lem  2037  exsb  2039  2exsb  2040  eujust  2059  euf  2062  cbveu  2081  mor  2100  eu2  2102  mo4f  2118  eu4  2120  2exeu  2150  2eu4  2151  exists1  2154  abid  2197  eleq12i  2277  abeq2  2318  abeq2i  2320  clabel  2336  abid2f  2378  sbabel  2379  neeq12i  2397  neanior  2467  ralnex  2498  dfrex2dc  2501  ralinexa  2537  nfraldya  2545  nfrexdya  2546  r3al  2554  r19.26-2  2640  ralbiim  2645  ralnex2  2650  r19.43  2669  ralcomf  2672  rexcomf  2673  ralrot3  2676  rexrot4  2678  reean  2680  3reeanv  2682  rabbi  2689  cbvralf  2736  cbvrexf  2737  cbvreu  2743  cbvral2vw  2756  cbvrex2vw  2757  cbvral2v  2758  cbvrex2v  2759  cbvral3v  2760  cbvralsv  2761  cbvrexsv  2762  sbralie  2763  rabeq2i  2776  issetf  2787  2gencl  2813  3gencl  2814  ceqsex2  2821  ceqsex3v  2823  ceqsex6v  2825  ceqsex8v  2826  gencbvex  2827  gencbval  2829  spc2gv  2874  eqvincf  2908  ceqsrex2v  2915  clel5  2920  elrab2  2942  ralab  2943  ralrab  2944  rexab  2945  rexrab  2946  ralab2  2947  rexab2  2949  eueq3dc  2957  morex  2967  euind  2970  reu2  2971  reu6  2972  rmo4  2976  reu4  2977  reu7  2978  rmo3f  2980  rmo4f  2981  rmoim  2984  2reuswapdc  2987  reuind  2988  2rmorex  2989  sbcco  3030  sbccomlem  3083  sbccom  3084  ra5  3098  rmo3  3101  csbco  3114  csbcow  3115  sbnfc2  3165  csbabg  3166  cbvralcsf  3167  cbvrexcsf  3168  cbvreucsf  3169  dfss  3191  dfss2f  3195  ss2ab  3272  dfdif3  3294  difeqri  3304  ddifstab  3316  raldifb  3324  uneqri  3326  ssequn2  3357  unss  3358  rexun  3364  ralunb  3365  elin2  3372  ineqri  3377  dfss1  3388  dfss5  3389  dfss4st  3417  ssddif  3418  difin  3421  indif  3427  difundi  3436  indifdir  3440  symdifxor  3450  inrab2  3457  rabun2  3463  reuun2  3467  0el  3494  rabeq0  3501  abeq0  3502  disjr  3521  disj1  3522  undif4  3534  uneqdifeqim  3557  r19.2m  3558  r19.3rm  3560  r19.9rmv  3563  raaan  3577  pwss  3645  dfpr2  3665  rexdifpr  3674  ralsnsg  3683  ralsns  3684  eltpg  3691  eldiftp  3692  ralprg  3697  rexprg  3698  raltpg  3699  rextpg  3700  snprc  3711  rabrsndc  3714  euabsn2  3715  eusn  3720  eldifsn  3774  ssdifsn  3775  rexdifsn  3779  eqsnm  3812  tpss  3815  snsssn  3818  prel12  3828  preqsn  3832  oprcl  3860  pwtpss  3864  eluniab  3879  elunirab  3880  unipr  3881  dfnfc2  3885  uniun  3886  uniin  3887  uni0b  3892  unissb  3897  elintab  3913  elintrab  3914  ssintab  3919  ssintrab  3925  intun  3933  intpr  3934  elrint  3942  iuncom4  3951  iuneq2  3960  dfiun2g  3976  ssiinf  3994  iundif2ss  4010  elriin  4015  iunxiun  4026  pwssb  4030  elpwpw  4031  iunpwss  4036  dfdisj2  4040  disjiun  4057  cbvopab1  4136  dftr5  4164  trint  4176  inex1  4197  inuni  4218  repizf2lem  4224  unidif0  4230  axpweq  4234  bnd2  4236  exmid01  4261  zfpair2  4273  exss  4292  elop  4296  opm  4299  otth  4307  copsex4g  4312  opeqsn  4318  opelopabsbALT  4326  brabga  4331  opelopabaf  4341  iunopab  4349  pwunss  4351  pocl  4371  frirrg  4418  elsuci  4471  elsucg  4472  sucel  4478  unisucg  4482  uniuni  4519  reusv3  4528  iunpw  4548  setindel  4607  elirr  4610  en2lp  4623  ordpwsucss  4636  zfregfr  4643  tfi  4651  peano2  4664  peano5  4667  elxp  4713  opelxp  4726  brxp  4727  rabxp  4733  opthprc  4747  brab2a  4749  opeliunxp  4751  xpundi  4752  xpundir  4753  elvvv  4759  brinxp  4764  brab2ga  4771  0xp  4776  ssrel2  4786  eqrelrel  4797  reliun  4817  reluni  4819  raliunxp  4840  rexiunxp  4841  ralxpf  4845  rexxpf  4846  iunxpf  4847  relop  4849  elco  4865  elcnv  4876  elcnv2  4877  dmin  4908  dmuni  4910  dmopab  4911  dmi  4915  dmmrnm  4919  rnopab  4947  elrnmpt1  4951  rncoeq  4974  resiexg  5026  restidsing  5037  dfima2  5046  dfima3  5047  elima2  5050  elima3  5051  imai  5060  elimasn  5071  epini  5075  dfse2  5077  cotr  5086  issref  5087  intasym  5089  asymref  5090  cnvopab  5106  cnvi  5109  cnvdif  5111  imainss  5120  rnxpid  5139  dfrel2  5155  dfrel3  5162  dmsnm  5170  rnsnm  5171  relsn2m  5175  dmsnopg  5176  cnvcnvsn  5181  elxp4  5192  elxp5  5193  cnvresima  5194  mptpreima  5198  dfco2  5204  coundi  5206  coundir  5207  imaco  5210  coiun  5214  coi1  5220  relssdmrn  5225  relrelss  5231  unixpm  5240  ressn  5245  cnviinm  5246  cnvpom  5247  cnvsom  5248  cbviota  5259  iotass  5272  eliota  5282  dffun2  5304  dffun4  5305  dffun7  5321  dffun8  5322  dffun9  5323  funopab  5329  funun  5338  funcnvsn  5342  fntpg  5353  funcnv2  5357  funcnv  5358  fun2cnv  5361  fncnv  5363  fun11  5364  fununi  5365  imadiflem  5376  imadif  5377  imainlem  5378  funimaexglem  5380  fnunsn  5406  fnres  5416  fnopabg  5423  mptfng  5425  mptun  5431  fun  5473  fcnvres  5485  dff12  5506  f1cnvcnv  5518  funforn  5531  dff1o2  5553  dff1o5  5557  f1orn  5558  resdif  5570  ffoss  5580  f11o  5581  f1o00  5584  fo00  5585  elfv  5601  fv3  5626  nfvres  5637  eqfnfv3  5707  fneqeql  5716  unpreima  5733  respreima  5736  dffo3  5755  dffo5  5757  f1ompt  5759  ffnfvf  5767  fmptco  5774  funopdmsn  5792  ftpg  5796  fnressn  5798  idref  5853  abrexco  5856  dff13  5865  dff13f  5867  fliftel  5890  isoini  5915  eusvobj2  5960  acexmidlema  5965  acexmidlemb  5966  acexmidlemph  5967  acexmidlem2  5971  oprabid  6006  brabvv  6021  dfoprab2  6022  eqoprab2b  6033  dmoprab  6056  rnoprab  6058  eloprabga  6062  mpomptx  6066  resoprab  6071  ffnov  6079  elrnmpo  6089  ralrnmpo  6090  rexrnmpo  6091  ovid  6092  ovi3  6113  ov6g  6114  foov  6123  opabex3d  6236  opabex3  6237  abexssex  6240  oprabex3  6244  oprabrexex2  6245  fmpo  6317  xporderlem  6347  f1od2  6351  mpoxopovel  6357  brtpos2  6367  dmtpos  6372  tpostpos  6380  tpossym  6392  tposoprab  6396  dfsmo2  6403  tfrlem7  6433  tfrlem9  6435  tfr1onlemaccex  6464  tfrcllemaccex  6477  tfrcldm  6479  frecabex  6514  el1o  6553  dif1o  6554  dfer2  6651  brdifun  6677  eqerlem  6681  qsid  6717  iinerm  6724  riinerm  6725  erinxp  6726  brecop  6742  eroveu  6743  erovlem  6744  ecopovsym  6748  mapval2  6795  mapsn  6807  elixp  6822  ixpeq2  6829  ixpin  6840  ixpiinm  6841  mptelixpg  6851  ixpsnf1o  6853  domen  6870  isfi  6882  en1  6921  xpsnen  6948  xpcomco  6953  xpassen  6957  ssenen  6980  nneneq  6986  snnen2oprc  6989  ac6sfi  7028  exmidpw  7038  exmidpweq  7039  pw1dc1  7044  eldju  7203  djur  7204  eldju2ndl  7207  eldju2ndr  7208  finomni  7275  nninfwlporlemd  7307  nninfwlpoimlemg  7310  acfun  7357  pw1nel3  7384  sucpw1nel3  7386  ccfunen  7418  elni  7463  ltexpi  7492  enq0enq  7586  enq0ref  7588  enq0tr  7589  prarloclem3  7652  ltdfpr  7661  genpdflem  7662  genpassl  7679  genpassu  7680  nqprrnd  7698  nqprl  7706  nqpru  7707  ltexprlemopl  7756  ltexprlemopu  7758  ltexprlemdisj  7761  ltexprlemloc  7762  recexprlemdisj  7785  caucvgprprlemell  7840  caucvgprprlemelu  7841  suplocexprlemml  7871  suplocsrlemb  7961  opelcn  7981  elreal  7983  elreal2  7985  peano1nnnn  8007  axicn  8018  axaddf  8023  axmulf  8024  axprecex  8035  axpre-ltirr  8037  axpre-mulgt0  8042  axcaucvglemres  8054  axpre-suploc  8057  xrlenlt  8179  ltxrlt  8180  inelr  8699  reapcotr  8713  1nn  9089  elnnne0  9351  un0addcl  9370  un0mulcl  9371  elnnz  9424  elznn0nn  9428  elznn0  9429  elznn  9430  elz2  9486  zapne  9489  3halfnz  9512  prime  9514  raluz2  9742  rexuz2  9744  supinfneg  9758  infsupneg  9759  eluz2b2  9766  eluz2b3  9767  ublbneg  9776  elq  9785  qreccl  9805  elpq  9812  ralrp  9839  rexrp  9840  rpnegap  9850  ltxr  9939  xrnemnf  9941  xrltso  9960  icc0r  10090  divelunit  10166  fzprval  10246  fztpval  10247  elfz1b  10254  fz01or  10275  4fvwrd4  10304  fzolb  10318  fzolb2  10319  elfzo3  10328  fzouzsplit  10345  elfzo0z  10352  fzo0m  10359  fzind2  10412  ioo0  10446  ico0  10448  ioc0  10449  uzennn  10625  seq3f1olemp  10704  iswrd  11040  caucvgre  11458  cvg1nlemcau  11461  resqrexlemex  11502  climeu  11773  fsum2dlemstep  11911  expcnv  11981  prodsnf  12069  fprod2dlemstep  12099  divides  12266  m1exp1  12378  divalgb  12402  bitsval2  12421  bitsmod  12433  bitscmp  12435  bezoutlemnewy  12483  bezoutlemmain  12485  bezoutlemex  12488  dfgcd2  12501  nnwosdc  12526  lcmgcdlem  12565  isprm2  12605  isprm3  12606  isprm4  12607  isprm5  12630  sqrt2irr  12650  oddpwdc  12662  pythagtriplem19  12771  pythagtrip  12772  pceu  12784  dvdsprmpweqnn  12825  4sqlem2  12878  4sqlem12  12891  dec5dvds2  12902  ennnfoneleminc  12948  ennnfonelemex  12951  ennnfonelemr  12960  ctiunct  12977  infpn2  12993  xpsfrnel  13343  xpsfrnel2  13345  gsum0g  13395  ismnd  13418  dfgrp2e  13527  dfgrp3me  13599  isnsg2  13706  eqger  13727  isabl2  13797  imasabl  13839  isrhm  14087  isrim  14098  isnzr2  14113  lss1d  14312  istps  14671  istps2  14672  isbasis2g  14684  tgval2  14690  txuni2  14895  tx1cn  14908  tx2cn  14909  uptx  14913  txdis1cn  14917  blres  15073  xmeterval  15074  xmeter  15075  isxms2  15091  isms2  15093  metrest  15145  qtopbasss  15160  dedekindicclemicc  15271  limcdifap  15301  plyrecj  15402  pilem1  15418  sincosq1lem  15464  mpodvdsmulf1o  15629  gausslemma2dlem1a  15702  gausslemma2dlem4  15708  lgsquadlem1  15721  lgsquadlem2  15722  2lgslem1b  15733  2sqlem1  15758  upgrex  15868  decidr  16070  bdcuni  16149  bdcriota  16156  bdinex1  16172  bj-zfpair2  16183  bj-axun2  16188  bj-ssom  16209  ss1oel2o  16265  nninfsellemdc  16287  nninfsellemsuc  16289  nninfsellemqall  16292  trirec0xor  16324  iswomni0  16330