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  682  mt2bi  684  orbi12i  764  or42  772  pm5.53  802  orddi  820  anddi  821  pm2.1dc  837  dcim  841  notnotrdc  843  dcnnOLD  849  rbaib  921  rbaibr  922  pm4.43  949  orbididc  953  pm5.75  962  3orass  981  3anass  982  3ancomb  986  3anan32  989  3anan12  990  anandi3  991  anandi3r  992  xordc  1392  falbitru  1417  19.26-2  1482  19.26-3an  1483  alrot3  1485  albiim  1487  2albiim  1488  19.27h  1560  19.27  1561  19.28h  1562  19.28  1563  nfalt  1578  aaanh  1586  aaan  1587  alinexa  1603  19.21-2  1667  nf2  1668  19.44  1682  19.45  1683  exrot3  1690  exrot4  1691  eeor  1695  sbcof2  1810  sbid2h  1849  19.23vv  1884  sbnv  1888  sblimv  1894  pm11.53  1895  19.41vv  1903  19.41vvv  1904  19.41vvvv  1905  exdistrv  1910  19.42vv  1911  19.42vvv  1912  19.42vvvv  1913  4exdistr  1916  cbvex4v  1930  eean  1931  sbn  1952  sbim  1953  sbor  1954  sban  1955  sbrim  1956  sblim  1957  sbbi  1959  sblbis  1960  sbrbis  1961  sbrbif  1962  sbco2d  1966  sbco2vd  1967  sbnf2  1981  2sb5  1983  2sb6  1984  sbcom2v  1985  sbcom2v2  1986  sbcom2  1987  sb6a  1988  2sb5rf  1989  2sb6rf  1990  sbalyz  1999  sbal  2000  sbal1yz  2001  sbex  2004  sbalv  2005  sbco4lem  2006  exsb  2008  2exsb  2009  eujust  2028  euf  2031  cbveu  2050  mor  2068  eu2  2070  mo4f  2086  eu4  2088  2exeu  2118  2eu4  2119  exists1  2122  abid  2165  eleq12i  2245  abeq2  2286  abeq2i  2288  clabel  2304  abid2f  2345  sbabel  2346  neeq12i  2364  neanior  2434  ralnex  2465  dfrex2dc  2468  ralinexa  2504  nfraldya  2512  nfrexdya  2513  r3al  2521  r19.26-2  2606  ralbiim  2611  ralnex2  2616  r19.43  2635  ralcomf  2638  rexcomf  2639  rexrot4  2643  reean  2645  3reeanv  2647  rabbi  2654  cbvralf  2696  cbvrexf  2697  cbvreu  2701  cbvral2vw  2714  cbvrex2vw  2715  cbvral2v  2716  cbvrex2v  2717  cbvral3v  2718  cbvralsv  2719  cbvrexsv  2720  sbralie  2721  rabeq2i  2734  issetf  2744  2gencl  2770  3gencl  2771  ceqsex2  2777  ceqsex3v  2779  ceqsex6v  2781  ceqsex8v  2782  gencbvex  2783  gencbval  2785  spc2gv  2828  eqvincf  2862  ceqsrex2v  2869  clel5  2874  elrab2  2896  ralab  2897  ralrab  2898  rexab  2899  rexrab  2900  ralab2  2901  rexab2  2903  eueq3dc  2911  morex  2921  euind  2924  reu2  2925  reu6  2926  rmo4  2930  reu4  2931  reu7  2932  rmo3f  2934  rmo4f  2935  rmoim  2938  2reuswapdc  2941  reuind  2942  2rmorex  2943  sbcco  2984  sbccomlem  3037  sbccom  3038  ra5  3051  rmo3  3054  csbco  3067  csbcow  3068  sbnfc2  3117  csbabg  3118  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  dfss  3143  dfss2f  3146  ss2ab  3223  dfdif3  3245  difeqri  3255  ddifstab  3267  raldifb  3275  uneqri  3277  ssequn2  3308  unss  3309  rexun  3315  ralunb  3316  elin2  3323  ineqri  3328  dfss1  3339  dfss5  3340  dfss4st  3368  ssddif  3369  difin  3372  indif  3378  difundi  3387  indifdir  3391  symdifxor  3401  inrab2  3408  rabun2  3414  reuun2  3418  0el  3445  rabeq0  3452  abeq0  3453  disjr  3472  disj1  3473  undif4  3485  uneqdifeqim  3508  r19.2m  3509  r19.3rm  3511  r19.9rmv  3514  raaan  3529  pwss  3591  dfpr2  3611  rexdifpr  3620  ralsnsg  3629  ralsns  3630  eltpg  3637  eldiftp  3638  ralprg  3643  rexprg  3644  raltpg  3645  rextpg  3646  snprc  3657  rabrsndc  3660  euabsn2  3661  eusn  3666  eldifsn  3719  ssdifsn  3720  rexdifsn  3724  eqsnm  3755  tpss  3758  snsssn  3761  prel12  3771  preqsn  3775  oprcl  3802  pwtpss  3806  eluniab  3821  elunirab  3822  unipr  3823  dfnfc2  3827  uniun  3828  uniin  3829  uni0b  3834  unissb  3839  elintab  3855  elintrab  3856  ssintab  3861  ssintrab  3867  intun  3875  intpr  3876  elrint  3884  iuncom4  3893  iuneq2  3902  dfiun2g  3918  ssiinf  3936  iundif2ss  3952  elriin  3957  iunxiun  3968  pwssb  3972  elpwpw  3973  iunpwss  3978  dfdisj2  3982  disjiun  3998  cbvopab1  4076  dftr5  4104  trint  4116  inex1  4137  inuni  4155  repizf2lem  4161  unidif0  4167  axpweq  4171  bnd2  4173  exmid01  4198  zfpair2  4210  exss  4227  elop  4231  opm  4234  otth  4242  copsex4g  4247  opeqsn  4252  opelopabsbALT  4259  brabga  4264  opelopabaf  4273  iunopab  4281  pwunss  4283  pocl  4303  frirrg  4350  elsuci  4403  elsucg  4404  sucel  4410  unisucg  4414  uniuni  4451  reusv3  4460  iunpw  4480  setindel  4537  elirr  4540  en2lp  4553  ordpwsucss  4566  zfregfr  4573  tfi  4581  peano2  4594  peano5  4597  elxp  4643  opelxp  4656  brxp  4657  rabxp  4663  opthprc  4677  brab2a  4679  opeliunxp  4681  xpundi  4682  xpundir  4683  elvvv  4689  brinxp  4694  brab2ga  4701  0xp  4706  ssrel2  4716  eqrelrel  4727  reliun  4747  reluni  4749  raliunxp  4768  rexiunxp  4769  ralxpf  4773  rexxpf  4774  iunxpf  4775  relop  4777  elco  4793  elcnv  4804  elcnv2  4805  dmin  4835  dmuni  4837  dmopab  4838  dmi  4842  dmmrnm  4846  rnopab  4874  elrnmpt1  4878  rncoeq  4900  resiexg  4952  restidsing  4963  dfima2  4972  dfima3  4973  elima2  4976  elima3  4977  imai  4984  elimasn  4995  epini  4999  dfse2  5001  cotr  5010  issref  5011  intasym  5013  asymref  5014  cnvopab  5030  cnvi  5033  cnvdif  5035  imainss  5044  rnxpid  5063  dfrel2  5079  dfrel3  5086  dmsnm  5094  rnsnm  5095  relsn2m  5099  dmsnopg  5100  cnvcnvsn  5105  elxp4  5116  elxp5  5117  cnvresima  5118  mptpreima  5122  dfco2  5128  coundi  5130  coundir  5131  imaco  5134  coiun  5138  coi1  5144  relssdmrn  5149  relrelss  5155  unixpm  5164  ressn  5169  cnviinm  5170  cnvpom  5171  cnvsom  5172  cbviota  5183  iotass  5195  eliota  5204  dffun2  5226  dffun4  5227  dffun7  5243  dffun8  5244  dffun9  5245  funopab  5251  funun  5260  funcnvsn  5261  fntpg  5272  funcnv2  5276  funcnv  5277  fun2cnv  5280  fncnv  5282  fun11  5283  fununi  5284  imadiflem  5295  imadif  5296  imainlem  5297  funimaexglem  5299  fnunsn  5323  fnres  5332  fnopabg  5339  mptfng  5341  mptun  5347  fun  5388  fcnvres  5399  dff12  5420  f1cnvcnv  5432  funforn  5445  dff1o2  5466  dff1o5  5470  f1orn  5471  resdif  5483  ffoss  5493  f11o  5494  f1o00  5496  fo00  5497  elfv  5513  fv3  5538  nfvres  5548  eqfnfv3  5615  fneqeql  5624  unpreima  5641  respreima  5644  dffo3  5663  dffo5  5665  f1ompt  5667  ffnfvf  5675  fmptco  5682  ftpg  5700  fnressn  5702  idref  5757  abrexco  5759  dff13  5768  dff13f  5770  fliftel  5793  isoini  5818  eusvobj2  5860  acexmidlema  5865  acexmidlemb  5866  acexmidlemph  5867  acexmidlem2  5871  oprabid  5906  brabvv  5920  dfoprab2  5921  eqoprab2b  5932  dmoprab  5955  rnoprab  5957  eloprabga  5961  mpomptx  5965  resoprab  5970  ffnov  5978  elrnmpo  5987  ralrnmpo  5988  rexrnmpo  5989  ovid  5990  ovi3  6010  ov6g  6011  foov  6020  opabex3d  6121  opabex3  6122  abexssex  6125  oprabex3  6129  oprabrexex2  6130  fmpo  6201  xporderlem  6231  f1od2  6235  mpoxopovel  6241  brtpos2  6251  dmtpos  6256  tpostpos  6264  tpossym  6276  tposoprab  6280  dfsmo2  6287  tfrlem7  6317  tfrlem9  6319  tfr1onlemaccex  6348  tfrcllemaccex  6361  tfrcldm  6363  frecabex  6398  el1o  6437  dif1o  6438  dfer2  6535  brdifun  6561  eqerlem  6565  qsid  6599  iinerm  6606  riinerm  6607  erinxp  6608  brecop  6624  eroveu  6625  erovlem  6626  ecopovsym  6630  mapval2  6677  mapsn  6689  elixp  6704  ixpeq2  6711  ixpin  6722  ixpiinm  6723  mptelixpg  6733  ixpsnf1o  6735  domen  6750  isfi  6760  en1  6798  xpsnen  6820  xpcomco  6825  xpassen  6829  ssenen  6850  nneneq  6856  snnen2oprc  6859  ac6sfi  6897  exmidpw  6907  exmidpweq  6908  pw1dc1  6912  eldju  7066  djur  7067  eldju2ndl  7070  eldju2ndr  7071  finomni  7137  nninfwlporlemd  7169  nninfwlpoimlemg  7172  acfun  7205  pw1nel3  7229  sucpw1nel3  7231  ccfunen  7262  elni  7306  ltexpi  7335  enq0enq  7429  enq0ref  7431  enq0tr  7432  prarloclem3  7495  ltdfpr  7504  genpdflem  7505  genpassl  7522  genpassu  7523  nqprrnd  7541  nqprl  7549  nqpru  7550  ltexprlemopl  7599  ltexprlemopu  7601  ltexprlemdisj  7604  ltexprlemloc  7605  recexprlemdisj  7628  caucvgprprlemell  7683  caucvgprprlemelu  7684  suplocexprlemml  7714  suplocsrlemb  7804  opelcn  7824  elreal  7826  elreal2  7828  peano1nnnn  7850  axicn  7861  axaddf  7866  axmulf  7867  axprecex  7878  axpre-ltirr  7880  axpre-mulgt0  7885  axcaucvglemres  7897  axpre-suploc  7900  xrlenlt  8021  ltxrlt  8022  inelr  8540  reapcotr  8554  1nn  8929  elnnne0  9189  un0addcl  9208  un0mulcl  9209  elnnz  9262  elznn0nn  9266  elznn0  9267  elznn  9268  elz2  9323  zapne  9326  3halfnz  9349  prime  9351  raluz2  9578  rexuz2  9580  supinfneg  9594  infsupneg  9595  eluz2b2  9602  eluz2b3  9603  ublbneg  9612  elq  9621  qreccl  9641  elpq  9647  ralrp  9674  rexrp  9675  rpnegap  9685  ltxr  9774  xrnemnf  9776  xrltso  9795  icc0r  9925  divelunit  10001  fzprval  10081  fztpval  10082  elfz1b  10089  fz01or  10110  4fvwrd4  10139  fzolb  10152  fzolb2  10153  elfzo3  10162  fzouzsplit  10178  elfzo0z  10183  fzo0m  10190  fzind2  10238  ioo0  10259  ico0  10261  ioc0  10262  uzennn  10435  seq3f1olemp  10501  caucvgre  10989  cvg1nlemcau  10992  resqrexlemex  11033  climeu  11303  fsum2dlemstep  11441  expcnv  11511  prodsnf  11599  fprod2dlemstep  11629  divides  11795  m1exp1  11905  divalgb  11929  bezoutlemnewy  11996  bezoutlemmain  11998  bezoutlemex  12001  dfgcd2  12014  nnwosdc  12039  lcmgcdlem  12076  isprm2  12116  isprm3  12117  isprm4  12118  isprm5  12141  sqrt2irr  12161  oddpwdc  12173  pythagtriplem19  12281  pythagtrip  12282  pceu  12294  dvdsprmpweqnn  12334  4sqlem2  12386  ennnfoneleminc  12411  ennnfonelemex  12414  ennnfonelemr  12423  ctiunct  12440  infpn2  12456  xpsfrnel  12762  xpsfrnel2  12764  ismnd  12819  dfgrp2e  12902  dfgrp3me  12969  isnsg2  13061  eqger  13081  isabl2  13095  istps  13502  istps2  13503  isbasis2g  13515  tgval2  13521  txuni2  13726  tx1cn  13739  tx2cn  13740  uptx  13744  txdis1cn  13748  blres  13904  xmeterval  13905  xmeter  13906  isxms2  13922  isms2  13924  metrest  13976  qtopbasss  13991  dedekindicclemicc  14080  limcdifap  14101  pilem1  14170  sincosq1lem  14216  2sqlem1  14431  decidr  14518  bdcuni  14598  bdcriota  14605  bdinex1  14621  bj-zfpair2  14632  bj-axun2  14637  bj-ssom  14658  ss1oel2o  14713  nninfsellemdc  14729  nninfsellemsuc  14731  nninfsellemqall  14734  trirec0xor  14763  iswomni0  14769