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  683  mt2bi  685  orbi12i  765  or42  773  pm5.53  803  orddi  821  anddi  822  pm2.1dc  838  dcim  842  notnotrdc  844  dcnnOLD  850  rbaib  922  rbaibr  923  pm4.43  950  orbididc  954  pm5.75  963  3orass  982  3anass  983  3ancomb  987  3anan32  990  3anan12  991  anandi3  992  anandi3r  993  xordc  1402  falbitru  1427  19.26-2  1492  19.26-3an  1493  alrot3  1495  albiim  1497  2albiim  1498  19.27h  1570  19.27  1571  19.28h  1572  19.28  1573  nfalt  1588  aaanh  1596  aaan  1597  alinexa  1613  19.21-2  1677  nf2  1678  19.44  1692  19.45  1693  exrot3  1700  exrot4  1701  eeor  1705  sbcof2  1820  sbid2h  1859  19.23vv  1894  sbnv  1898  sblimv  1904  pm11.53  1905  19.41vv  1913  19.41vvv  1914  19.41vvvv  1915  exdistrv  1920  19.42vv  1921  19.42vvv  1922  19.42vvvv  1923  4exdistr  1926  cbvex4v  1940  eean  1941  sbn  1962  sbim  1963  sbor  1964  sban  1965  sbrim  1966  sblim  1967  sbbi  1969  sblbis  1970  sbrbis  1971  sbrbif  1972  sbco2d  1976  sbco2vd  1977  sbnf2  1991  2sb5  1993  2sb6  1994  sbcom2v  1995  sbcom2v2  1996  sbcom2  1997  sb6a  1998  2sb5rf  1999  2sb6rf  2000  sbalyz  2009  sbal  2010  sbal1yz  2011  sbex  2014  sbalv  2015  sbco4lem  2016  exsb  2018  2exsb  2019  eujust  2038  euf  2041  cbveu  2060  mor  2078  eu2  2080  mo4f  2096  eu4  2098  2exeu  2128  2eu4  2129  exists1  2132  abid  2175  eleq12i  2255  abeq2  2296  abeq2i  2298  clabel  2314  abid2f  2355  sbabel  2356  neeq12i  2374  neanior  2444  ralnex  2475  dfrex2dc  2478  ralinexa  2514  nfraldya  2522  nfrexdya  2523  r3al  2531  r19.26-2  2616  ralbiim  2621  ralnex2  2626  r19.43  2645  ralcomf  2648  rexcomf  2649  ralrot3  2652  rexrot4  2654  reean  2656  3reeanv  2658  rabbi  2665  cbvralf  2707  cbvrexf  2708  cbvreu  2713  cbvral2vw  2726  cbvrex2vw  2727  cbvral2v  2728  cbvrex2v  2729  cbvral3v  2730  cbvralsv  2731  cbvrexsv  2732  sbralie  2733  rabeq2i  2746  issetf  2756  2gencl  2782  3gencl  2783  ceqsex2  2789  ceqsex3v  2791  ceqsex6v  2793  ceqsex8v  2794  gencbvex  2795  gencbval  2797  spc2gv  2840  eqvincf  2874  ceqsrex2v  2881  clel5  2886  elrab2  2908  ralab  2909  ralrab  2910  rexab  2911  rexrab  2912  ralab2  2913  rexab2  2915  eueq3dc  2923  morex  2933  euind  2936  reu2  2937  reu6  2938  rmo4  2942  reu4  2943  reu7  2944  rmo3f  2946  rmo4f  2947  rmoim  2950  2reuswapdc  2953  reuind  2954  2rmorex  2955  sbcco  2996  sbccomlem  3049  sbccom  3050  ra5  3063  rmo3  3066  csbco  3079  csbcow  3080  sbnfc2  3129  csbabg  3130  cbvralcsf  3131  cbvrexcsf  3132  cbvreucsf  3133  dfss  3155  dfss2f  3158  ss2ab  3235  dfdif3  3257  difeqri  3267  ddifstab  3279  raldifb  3287  uneqri  3289  ssequn2  3320  unss  3321  rexun  3327  ralunb  3328  elin2  3335  ineqri  3340  dfss1  3351  dfss5  3352  dfss4st  3380  ssddif  3381  difin  3384  indif  3390  difundi  3399  indifdir  3403  symdifxor  3413  inrab2  3420  rabun2  3426  reuun2  3430  0el  3457  rabeq0  3464  abeq0  3465  disjr  3484  disj1  3485  undif4  3497  uneqdifeqim  3520  r19.2m  3521  r19.3rm  3523  r19.9rmv  3526  raaan  3541  pwss  3603  dfpr2  3623  rexdifpr  3632  ralsnsg  3641  ralsns  3642  eltpg  3649  eldiftp  3650  ralprg  3655  rexprg  3656  raltpg  3657  rextpg  3658  snprc  3669  rabrsndc  3672  euabsn2  3673  eusn  3678  eldifsn  3731  ssdifsn  3732  rexdifsn  3736  eqsnm  3767  tpss  3770  snsssn  3773  prel12  3783  preqsn  3787  oprcl  3814  pwtpss  3818  eluniab  3833  elunirab  3834  unipr  3835  dfnfc2  3839  uniun  3840  uniin  3841  uni0b  3846  unissb  3851  elintab  3867  elintrab  3868  ssintab  3873  ssintrab  3879  intun  3887  intpr  3888  elrint  3896  iuncom4  3905  iuneq2  3914  dfiun2g  3930  ssiinf  3948  iundif2ss  3964  elriin  3969  iunxiun  3980  pwssb  3984  elpwpw  3985  iunpwss  3990  dfdisj2  3994  disjiun  4010  cbvopab1  4088  dftr5  4116  trint  4128  inex1  4149  inuni  4167  repizf2lem  4173  unidif0  4179  axpweq  4183  bnd2  4185  exmid01  4210  zfpair2  4222  exss  4239  elop  4243  opm  4246  otth  4254  copsex4g  4259  opeqsn  4264  opelopabsbALT  4271  brabga  4276  opelopabaf  4285  iunopab  4293  pwunss  4295  pocl  4315  frirrg  4362  elsuci  4415  elsucg  4416  sucel  4422  unisucg  4426  uniuni  4463  reusv3  4472  iunpw  4492  setindel  4549  elirr  4552  en2lp  4565  ordpwsucss  4578  zfregfr  4585  tfi  4593  peano2  4606  peano5  4609  elxp  4655  opelxp  4668  brxp  4669  rabxp  4675  opthprc  4689  brab2a  4691  opeliunxp  4693  xpundi  4694  xpundir  4695  elvvv  4701  brinxp  4706  brab2ga  4713  0xp  4718  ssrel2  4728  eqrelrel  4739  reliun  4759  reluni  4761  raliunxp  4780  rexiunxp  4781  ralxpf  4785  rexxpf  4786  iunxpf  4787  relop  4789  elco  4805  elcnv  4816  elcnv2  4817  dmin  4847  dmuni  4849  dmopab  4850  dmi  4854  dmmrnm  4858  rnopab  4886  elrnmpt1  4890  rncoeq  4912  resiexg  4964  restidsing  4975  dfima2  4984  dfima3  4985  elima2  4988  elima3  4989  imai  4996  elimasn  5007  epini  5011  dfse2  5013  cotr  5022  issref  5023  intasym  5025  asymref  5026  cnvopab  5042  cnvi  5045  cnvdif  5047  imainss  5056  rnxpid  5075  dfrel2  5091  dfrel3  5098  dmsnm  5106  rnsnm  5107  relsn2m  5111  dmsnopg  5112  cnvcnvsn  5117  elxp4  5128  elxp5  5129  cnvresima  5130  mptpreima  5134  dfco2  5140  coundi  5142  coundir  5143  imaco  5146  coiun  5150  coi1  5156  relssdmrn  5161  relrelss  5167  unixpm  5176  ressn  5181  cnviinm  5182  cnvpom  5183  cnvsom  5184  cbviota  5195  iotass  5207  eliota  5216  dffun2  5238  dffun4  5239  dffun7  5255  dffun8  5256  dffun9  5257  funopab  5263  funun  5272  funcnvsn  5273  fntpg  5284  funcnv2  5288  funcnv  5289  fun2cnv  5292  fncnv  5294  fun11  5295  fununi  5296  imadiflem  5307  imadif  5308  imainlem  5309  funimaexglem  5311  fnunsn  5335  fnres  5344  fnopabg  5351  mptfng  5353  mptun  5359  fun  5400  fcnvres  5411  dff12  5432  f1cnvcnv  5444  funforn  5457  dff1o2  5478  dff1o5  5482  f1orn  5483  resdif  5495  ffoss  5505  f11o  5506  f1o00  5508  fo00  5509  elfv  5525  fv3  5550  nfvres  5560  eqfnfv3  5628  fneqeql  5637  unpreima  5654  respreima  5657  dffo3  5676  dffo5  5678  f1ompt  5680  ffnfvf  5688  fmptco  5695  ftpg  5713  fnressn  5715  idref  5770  abrexco  5773  dff13  5782  dff13f  5784  fliftel  5807  isoini  5832  eusvobj2  5874  acexmidlema  5879  acexmidlemb  5880  acexmidlemph  5881  acexmidlem2  5885  oprabid  5920  brabvv  5934  dfoprab2  5935  eqoprab2b  5946  dmoprab  5969  rnoprab  5971  eloprabga  5975  mpomptx  5979  resoprab  5984  ffnov  5992  elrnmpo  6001  ralrnmpo  6002  rexrnmpo  6003  ovid  6004  ovi3  6024  ov6g  6025  foov  6034  opabex3d  6135  opabex3  6136  abexssex  6139  oprabex3  6143  oprabrexex2  6144  fmpo  6215  xporderlem  6245  f1od2  6249  mpoxopovel  6255  brtpos2  6265  dmtpos  6270  tpostpos  6278  tpossym  6290  tposoprab  6294  dfsmo2  6301  tfrlem7  6331  tfrlem9  6333  tfr1onlemaccex  6362  tfrcllemaccex  6375  tfrcldm  6377  frecabex  6412  el1o  6451  dif1o  6452  dfer2  6549  brdifun  6575  eqerlem  6579  qsid  6613  iinerm  6620  riinerm  6621  erinxp  6622  brecop  6638  eroveu  6639  erovlem  6640  ecopovsym  6644  mapval2  6691  mapsn  6703  elixp  6718  ixpeq2  6725  ixpin  6736  ixpiinm  6737  mptelixpg  6747  ixpsnf1o  6749  domen  6764  isfi  6774  en1  6812  xpsnen  6834  xpcomco  6839  xpassen  6843  ssenen  6864  nneneq  6870  snnen2oprc  6873  ac6sfi  6911  exmidpw  6921  exmidpweq  6922  pw1dc1  6926  eldju  7080  djur  7081  eldju2ndl  7084  eldju2ndr  7085  finomni  7151  nninfwlporlemd  7183  nninfwlpoimlemg  7186  acfun  7219  pw1nel3  7243  sucpw1nel3  7245  ccfunen  7276  elni  7320  ltexpi  7349  enq0enq  7443  enq0ref  7445  enq0tr  7446  prarloclem3  7509  ltdfpr  7518  genpdflem  7519  genpassl  7536  genpassu  7537  nqprrnd  7555  nqprl  7563  nqpru  7564  ltexprlemopl  7613  ltexprlemopu  7615  ltexprlemdisj  7618  ltexprlemloc  7619  recexprlemdisj  7642  caucvgprprlemell  7697  caucvgprprlemelu  7698  suplocexprlemml  7728  suplocsrlemb  7818  opelcn  7838  elreal  7840  elreal2  7842  peano1nnnn  7864  axicn  7875  axaddf  7880  axmulf  7881  axprecex  7892  axpre-ltirr  7894  axpre-mulgt0  7899  axcaucvglemres  7911  axpre-suploc  7914  xrlenlt  8035  ltxrlt  8036  inelr  8554  reapcotr  8568  1nn  8943  elnnne0  9203  un0addcl  9222  un0mulcl  9223  elnnz  9276  elznn0nn  9280  elznn0  9281  elznn  9282  elz2  9337  zapne  9340  3halfnz  9363  prime  9365  raluz2  9592  rexuz2  9594  supinfneg  9608  infsupneg  9609  eluz2b2  9616  eluz2b3  9617  ublbneg  9626  elq  9635  qreccl  9655  elpq  9661  ralrp  9688  rexrp  9689  rpnegap  9699  ltxr  9788  xrnemnf  9790  xrltso  9809  icc0r  9939  divelunit  10015  fzprval  10095  fztpval  10096  elfz1b  10103  fz01or  10124  4fvwrd4  10153  fzolb  10166  fzolb2  10167  elfzo3  10176  fzouzsplit  10192  elfzo0z  10197  fzo0m  10204  fzind2  10252  ioo0  10273  ico0  10275  ioc0  10276  uzennn  10449  seq3f1olemp  10515  caucvgre  11003  cvg1nlemcau  11006  resqrexlemex  11047  climeu  11317  fsum2dlemstep  11455  expcnv  11525  prodsnf  11613  fprod2dlemstep  11643  divides  11809  m1exp1  11919  divalgb  11943  bezoutlemnewy  12010  bezoutlemmain  12012  bezoutlemex  12015  dfgcd2  12028  nnwosdc  12053  lcmgcdlem  12090  isprm2  12130  isprm3  12131  isprm4  12132  isprm5  12155  sqrt2irr  12175  oddpwdc  12187  pythagtriplem19  12295  pythagtrip  12296  pceu  12308  dvdsprmpweqnn  12348  4sqlem2  12400  ennnfoneleminc  12425  ennnfonelemex  12428  ennnfonelemr  12437  ctiunct  12454  infpn2  12470  xpsfrnel  12781  xpsfrnel2  12783  ismnd  12841  dfgrp2e  12924  dfgrp3me  12996  isnsg2  13094  eqger  13115  isabl2  13130  lss1d  13567  istps  13803  istps2  13804  isbasis2g  13816  tgval2  13822  txuni2  14027  tx1cn  14040  tx2cn  14041  uptx  14045  txdis1cn  14049  blres  14205  xmeterval  14206  xmeter  14207  isxms2  14223  isms2  14225  metrest  14277  qtopbasss  14292  dedekindicclemicc  14381  limcdifap  14402  pilem1  14471  sincosq1lem  14517  2sqlem1  14732  decidr  14819  bdcuni  14899  bdcriota  14906  bdinex1  14922  bj-zfpair2  14933  bj-axun2  14938  bj-ssom  14959  ss1oel2o  15015  nninfsellemdc  15031  nninfsellemsuc  15033  nninfsellemqall  15036  trirec0xor  15065  iswomni0  15071