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  589  xchbinx  689  mt2bi  691  orbi12i  772  or42  780  pm5.53  810  orddi  828  anddi  829  pm2.1dc  845  dcim  849  notnotrdc  851  dcnnOLD  857  rbaib  929  rbaibr  930  pm4.43  958  orbididc  962  pm5.75  971  ifptru  998  ifpfal  999  3orass  1008  3anass  1009  3ancomb  1013  3anan32  1016  3anan12  1017  anandi3  1018  anandi3r  1019  xordc  1437  falbitru  1462  19.26-2  1531  19.26-3an  1532  alrot3  1534  albiim  1536  2albiim  1537  19.27h  1609  19.27  1610  19.28h  1611  19.28  1612  nfalt  1627  aaanh  1635  aaan  1636  alinexa  1652  19.21-2  1715  nf2  1716  19.44  1730  19.45  1731  exrot3  1738  exrot4  1739  eeor  1743  sbcof2  1859  sbid2h  1898  19.23vv  1933  sbnv  1939  sblimv  1946  pm11.53  1947  19.41vv  1955  19.41vvv  1956  19.41vvvv  1957  exdistrv  1962  19.42vv  1963  19.42vvv  1964  19.42vvvv  1965  4exdistr  1968  cbvex4v  1986  eean  1987  sbn  2008  sbim  2009  sbor  2010  sban  2011  sbrim  2012  sblim  2013  sbbi  2015  sblbis  2016  sbrbis  2017  sbrbif  2018  sbco2d  2022  sbco2vd  2023  sbnf2  2037  2sb5  2039  2sb6  2040  sbcom2v  2041  sbcom2v2  2042  sbcom2  2043  sb6a  2044  2sb5rf  2045  2sb6rf  2046  sbalyz  2055  sbal  2056  sbal1yz  2057  sbex  2060  sbalv  2061  sbco4lem  2062  exsb  2064  2exsb  2065  eujust  2084  euf  2087  cbveu  2106  mor  2125  eu2  2127  mo4f  2143  eu4  2145  2exeu  2175  2eu4  2176  exists1  2179  abid  2222  eleq12i  2302  abeq2  2343  abeq2i  2345  abbib  2352  clabel  2363  eqabb  2370  abid2f  2412  sbabel  2413  neeq12i  2431  neanior  2501  ralnex  2532  dfrex2dc  2535  ralinexa  2571  nfraldya  2579  nfrexdya  2580  r3al  2588  r19.26-2  2674  ralbiim  2679  ralnex2  2684  r19.43  2703  ralcomf  2706  rexcomf  2707  ralrot3  2710  rexrot4  2712  reean  2714  3reeanv  2716  reqabi  2722  rabbi  2724  cbvralf  2771  cbvrexf  2772  cbvreu  2778  cbvral2vw  2791  cbvrex2vw  2792  cbvral2v  2793  cbvrex2v  2794  cbvral3v  2795  cbvralsv  2796  cbvrexsv  2797  sbralie  2798  rabeq2i  2812  issetf  2823  2gencl  2849  3gencl  2850  ceqsex2  2857  ceqsex3v  2859  ceqsex6v  2861  ceqsex8v  2862  gencbvex  2863  gencbval  2865  spc2gv  2910  eqvincf  2944  ceqsrex2v  2951  clel5  2956  elrab2  2978  ralab  2979  ralrab  2980  rexab  2981  rexrab  2982  ralab2  2983  rexab2  2985  eueq3dc  2993  morex  3003  euind  3006  reu2  3007  reu6  3008  rmo4  3012  reu4  3013  reu7  3014  rmo3f  3016  rmo4f  3017  rmoim  3020  2reuswapdc  3023  reuind  3024  2rmorex  3025  sbcco  3066  sbccomlem  3119  sbccom  3120  ra5  3134  rmo3  3137  csbco  3150  csbcow  3151  sbnfc2  3201  csbabg  3202  cbvralcsf  3203  cbvrexcsf  3204  cbvreucsf  3205  dfss  3227  dfss2f  3231  ss2ab  3308  dfdif3  3331  difeqri  3341  ddifstab  3353  raldifb  3361  uneqri  3363  ssequn2  3394  unss  3395  rexun  3401  ralunb  3402  elin2  3409  ineqri  3416  dfss1  3427  dfss5  3428  dfss4st  3456  ssddif  3457  difin  3460  indif  3466  difundi  3475  indifdir  3479  symdifxor  3489  inrab2  3496  rabun2  3502  reuun2  3506  0el  3533  rabeq0  3540  abeq0  3541  disjr  3560  disj1  3561  undif4  3573  uneqdifeqim  3597  r19.2m  3598  r19.3rm  3600  r19.9rmv  3603  raaan  3617  pwss  3690  dfpr2  3710  rexdifpr  3719  ralsnsg  3728  ralsns  3729  eltpg  3736  eldiftp  3737  ralprg  3742  rexprg  3743  raltpg  3744  rextpg  3745  snprc  3756  rabrsndc  3761  euabsn2  3762  eusn  3767  eldifsn  3822  ssdifsn  3823  rexdifsn  3827  eqsnm  3861  tpss  3864  snsssn  3867  prel12  3877  preqsn  3881  oprcl  3909  pwtpss  3913  eluniab  3928  elunirab  3929  unipr  3930  dfnfc2  3934  uniun  3935  uniin  3936  uni0b  3941  unissb  3946  elintab  3962  elintrab  3963  ssintab  3968  ssintrab  3974  intun  3982  intpr  3983  elrint  3991  iuncom4  4000  iuneq2  4009  dfiun2g  4025  ssiinf  4043  iundif2ss  4059  elriin  4064  iunxiun  4075  pwssb  4079  elpwpw  4080  iunpwss  4085  dfdisj2  4089  disjiun  4106  cbvopab1  4185  dftr5  4213  trint  4225  inex1  4246  inuni  4269  repizf2lem  4276  unidif0  4282  axpweq  4286  bnd2  4288  exmid01  4313  zfpair2  4325  exss  4345  elop  4349  opm  4352  otth  4360  copsex4g  4365  opeqsn  4371  opelopabsbALT  4379  brabga  4384  opelopabaf  4394  iunopab  4402  pwunss  4406  pocl  4426  frirrg  4473  elsuci  4526  elsucg  4527  sucel  4533  unisucg  4537  uniuni  4574  reusv3  4583  iunpw  4603  setindel  4662  elirr  4665  en2lp  4678  ordpwsucss  4691  zfregfr  4698  tfi  4706  peano2  4719  peano5  4722  elxp  4768  opelxp  4781  brxp  4782  rabxp  4789  opthprc  4803  brab2a  4805  opeliunxp  4807  xpundi  4808  xpundir  4809  elvvv  4815  brinxp  4820  brab2ga  4827  0xp  4832  ssrel2  4842  eqrelrel  4853  reliun  4875  reluni  4877  raliunxp  4898  rexiunxp  4899  ralxpf  4903  rexxpf  4904  iunxpf  4905  relop  4907  elco  4923  elcnv  4934  elcnv2  4935  dmin  4966  dmuni  4968  dmopab  4969  dmi  4973  dmmrnm  4978  rnopab  5006  elrnmpt1  5010  rncoeq  5033  resiexg  5085  restidsing  5096  dfima2  5105  dfima3  5106  elima2  5109  elima3  5110  imai  5120  elimasn  5131  epini  5135  dfse2  5137  cotr  5146  issref  5147  intasym  5149  asymref  5150  cnvopab  5166  cnvi  5169  cnvdif  5171  imainss  5180  rnxpid  5199  dfrel2  5215  dfrel3  5222  dmsnm  5230  rnsnm  5231  relsn2m  5235  dmsnopg  5236  cnvcnvsn  5241  elxp4  5252  elxp5  5253  cnvresima  5254  mptpreima  5258  dfco2  5264  coundi  5266  coundir  5267  imaco  5270  coiun  5274  coi1  5280  relssdmrn  5285  relrelss  5291  unixpm  5300  ressn  5305  cnviinm  5306  cnvpom  5307  cnvsom  5308  cbviota  5319  iotass  5332  eliota  5342  dffun2  5364  dffun4  5365  dffun7  5381  dffun8  5382  dffun9  5383  funopab  5389  funun  5399  funcnvsn  5403  fntpg  5414  funcnv2  5418  funcnv  5419  fun2cnv  5422  fncnv  5424  fun11  5425  fununi  5426  imadiflem  5437  imadif  5438  imainlem  5439  funimaexglem  5441  fnunsn  5467  fnres  5477  fnopabg  5484  mptfng  5486  mptun  5492  fun  5538  fcnvres  5552  dff12  5574  f1cnvcnv  5586  funforn  5599  dff1o2  5621  dff1o5  5625  f1orn  5626  resdif  5638  ffoss  5649  f11o  5650  f1o00  5653  fo00  5654  elfv  5670  fv3  5695  nfvres  5708  eqfnfv3  5779  fneqeql  5788  unpreima  5804  respreima  5807  dffo3  5826  dffo5  5828  f1ompt  5830  ffnfvf  5838  fmptco  5845  funopdmsn  5866  ftpg  5870  fnressn  5872  idref  5931  abrexco  5934  dff13  5943  dff13f  5945  fliftel  5968  isoini  5993  eusvobj2  6038  acexmidlema  6043  acexmidlemb  6044  acexmidlemph  6045  acexmidlem2  6049  oprabid  6084  brabvv  6101  dfoprab2  6102  eqoprab2b  6113  dmoprab  6136  rnoprab  6138  eloprabga  6142  mpomptx  6146  resoprab  6151  ffnov  6159  elrnmpo  6169  ralrnmpo  6170  rexrnmpo  6171  ovid  6172  ovi3  6193  ov6g  6194  foov  6203  opabex3d  6316  opabex3  6317  abexssex  6320  oprabex3  6324  oprabrexex2  6325  fmpo  6399  xporderlem  6429  f1od2  6433  mpoxopovel  6474  brtpos2  6484  dmtpos  6489  tpostpos  6497  tpossym  6509  tposoprab  6513  dfsmo2  6520  tfrlem7  6550  tfrlem9  6552  tfr1onlemaccex  6581  tfrcllemaccex  6594  tfrcldm  6596  frecabex  6631  el1o  6672  dif1o  6673  dfer2  6770  brdifun  6796  eqerlem  6800  qsid  6836  iinerm  6843  riinerm  6844  erinxp  6845  brecop  6861  eroveu  6862  erovlem  6863  ecopovsym  6867  mapval2  6914  mapsn  6927  elixp  6942  ixpeq2  6949  ixpin  6960  ixpiinm  6961  mptelixpg  6971  ixpsnf1o  6973  domen  6990  isfi  7002  en1  7041  modom2  7064  xpsnen  7074  xpcomco  7079  xpassen  7083  ssenen  7107  nneneq  7113  snnen2oprc  7116  ac6sfi  7157  exmidpw  7170  exmidpweq  7171  pw1dc1  7176  elfpw  7217  eldju  7361  djur  7362  eldju2ndl  7365  eldju2ndr  7366  finomni  7433  nninfwlporlemd  7465  nninfwlpoimlemg  7468  acfun  7516  pw1nel3  7543  sucpw1nel3  7545  ccfunen  7583  elni  7628  ltexpi  7657  enq0enq  7751  enq0ref  7753  enq0tr  7754  prarloclem3  7817  ltdfpr  7826  genpdflem  7827  genpassl  7844  genpassu  7845  nqprrnd  7863  nqprl  7871  nqpru  7872  ltexprlemopl  7921  ltexprlemopu  7923  ltexprlemdisj  7926  ltexprlemloc  7927  recexprlemdisj  7950  caucvgprprlemell  8005  caucvgprprlemelu  8006  suplocexprlemml  8036  suplocsrlemb  8126  opelcn  8146  elreal  8148  elreal2  8150  peano1nnnn  8172  axicn  8183  axaddf  8188  axmulf  8189  axprecex  8200  axpre-ltirr  8202  axpre-mulgt0  8207  axcaucvglemres  8219  axpre-suploc  8222  xrlenlt  8343  ltxrlt  8344  inelr  8863  reapcotr  8877  1nn  9253  elnnne0  9515  un0addcl  9534  un0mulcl  9535  elnnz  9592  elznn0nn  9596  elznn0  9597  elznn  9598  elz2  9654  zapne  9657  3halfnz  9681  prime  9683  raluz2  9917  rexuz2  9919  supinfneg  9933  infsupneg  9934  eluz2b2  9941  eluz2b3  9942  ublbneg  9951  elq  9960  qreccl  9980  elpq  9987  ralrp  10014  rexrp  10015  rpnegap  10025  ltxr  10114  xrnemnf  10116  xrltso  10135  icc0r  10265  divelunit  10341  fzprval  10423  fztpval  10424  elfz1b  10431  fz01or  10452  4fvwrd4  10481  fzolb  10495  fzolb2  10496  elfzo3  10505  fzouzsplit  10522  elfzo0z  10530  fzo0m  10538  fzind2  10592  ioo0  10626  ico0  10628  ioc0  10629  uzennn  10805  seq3f1olemp  10884  sseqn  11211  hashfibc  11215  iswrd  11234  caucvgre  11674  cvg1nlemcau  11677  resqrexlemex  11718  climeu  11989  fsum2dlemstep  12128  expcnv  12198  prodsnf  12286  fprod2dlemstep  12316  divides  12483  m1exp1  12595  divalgb  12619  bitsval2  12638  bitsmod  12650  bitscmp  12652  bezoutlemnewy  12700  bezoutlemmain  12702  bezoutlemex  12705  dfgcd2  12718  nnwosdc  12743  lcmgcdlem  12782  isprm2  12822  isprm3  12823  isprm4  12824  isprm5  12847  sqrt2irr  12867  oddpwdc  12879  pythagtriplem19  12988  pythagtrip  12989  pceu  13001  dvdsprmpweqnn  13042  4sqlem2  13095  4sqlem12  13108  dec5dvds2  13119  ballotfilemodife  13162  ballotfilem4  13163  ennnfoneleminc  13183  ennnfonelemex  13186  ennnfonelemr  13195  ctiunct  13212  infpn2  13228  xpsfrnel  13578  xpsfrnel2  13580  gsum0g  13630  ismnd  13653  dfgrp2e  13762  dfgrp3me  13834  isnsg2  13941  eqger  13962  isabl2  14032  imasabl  14074  isrhm  14325  isrim  14336  isnzr2  14351  drngprop  14477  lss1d  14580  istps  14946  istps2  14947  isbasis2g  14959  tgval2  14965  txuni2  15170  tx1cn  15183  tx2cn  15184  uptx  15188  txdis1cn  15192  blres  15348  xmeterval  15349  xmeter  15350  isxms2  15366  isms2  15368  metrest  15420  qtopbasss  15435  dedekindicclemicc  15546  limcdifap  15576  plyrecj  15677  pilem1  15693  sincosq1lem  15739  mpodvdsmulf1o  15907  gausslemma2dlem1a  15980  gausslemma2dlem4  15986  lgsquadlem1  15999  lgsquadlem2  16000  2lgslem1b  16011  2sqlem1  16036  upgrex  16147  griedg0ssusgr  16295  clwwlkn1loopb  16464  clwwlknon2x  16479  decidr  16617  bdcuni  16695  bdcriota  16702  bdinex1  16718  bj-zfpair2  16729  bj-axun2  16734  bj-ssom  16755  ss1oel2o  16810  nninfsellemdc  16837  nninfsellemsuc  16839  nninfsellemqall  16842  trirec0xor  16878  iswomni0  16885