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  688  mt2bi  690  orbi12i  771  or42  779  pm5.53  809  orddi  827  anddi  828  pm2.1dc  844  dcim  848  notnotrdc  850  dcnnOLD  856  rbaib  928  rbaibr  929  pm4.43  957  orbididc  961  pm5.75  970  ifptru  997  ifpfal  998  3orass  1007  3anass  1008  3ancomb  1012  3anan32  1015  3anan12  1016  anandi3  1017  anandi3r  1018  xordc  1436  falbitru  1461  19.26-2  1530  19.26-3an  1531  alrot3  1533  albiim  1535  2albiim  1536  19.27h  1608  19.27  1609  19.28h  1610  19.28  1611  nfalt  1626  aaanh  1634  aaan  1635  alinexa  1651  19.21-2  1714  nf2  1715  19.44  1729  19.45  1730  exrot3  1737  exrot4  1738  eeor  1742  sbcof2  1857  sbid2h  1896  19.23vv  1931  sbnv  1936  sblimv  1942  pm11.53  1943  19.41vv  1951  19.41vvv  1952  19.41vvvv  1953  exdistrv  1958  19.42vv  1959  19.42vvv  1960  19.42vvvv  1961  4exdistr  1964  cbvex4v  1982  eean  1983  sbn  2004  sbim  2005  sbor  2006  sban  2007  sbrim  2008  sblim  2009  sbbi  2011  sblbis  2012  sbrbis  2013  sbrbif  2014  sbco2d  2018  sbco2vd  2019  sbnf2  2033  2sb5  2035  2sb6  2036  sbcom2v  2037  sbcom2v2  2038  sbcom2  2039  sb6a  2040  2sb5rf  2041  2sb6rf  2042  sbalyz  2051  sbal  2052  sbal1yz  2053  sbex  2056  sbalv  2057  sbco4lem  2058  exsb  2060  2exsb  2061  eujust  2080  euf  2083  cbveu  2102  mor  2121  eu2  2123  mo4f  2139  eu4  2141  2exeu  2171  2eu4  2172  exists1  2175  abid  2218  eleq12i  2298  abeq2  2339  abeq2i  2341  clabel  2357  abid2f  2399  sbabel  2400  neeq12i  2418  neanior  2488  ralnex  2519  dfrex2dc  2522  ralinexa  2558  nfraldya  2566  nfrexdya  2567  r3al  2575  r19.26-2  2661  ralbiim  2666  ralnex2  2671  r19.43  2690  ralcomf  2693  rexcomf  2694  ralrot3  2697  rexrot4  2699  reean  2701  3reeanv  2703  rabbi  2710  cbvralf  2757  cbvrexf  2758  cbvreu  2764  cbvral2vw  2777  cbvrex2vw  2778  cbvral2v  2779  cbvrex2v  2780  cbvral3v  2781  cbvralsv  2782  cbvrexsv  2783  sbralie  2784  rabeq2i  2798  issetf  2809  2gencl  2835  3gencl  2836  ceqsex2  2843  ceqsex3v  2845  ceqsex6v  2847  ceqsex8v  2848  gencbvex  2849  gencbval  2851  spc2gv  2896  eqvincf  2930  ceqsrex2v  2937  clel5  2942  elrab2  2964  ralab  2965  ralrab  2966  rexab  2967  rexrab  2968  ralab2  2969  rexab2  2971  eueq3dc  2979  morex  2989  euind  2992  reu2  2993  reu6  2994  rmo4  2998  reu4  2999  reu7  3000  rmo3f  3002  rmo4f  3003  rmoim  3006  2reuswapdc  3009  reuind  3010  2rmorex  3011  sbcco  3052  sbccomlem  3105  sbccom  3106  ra5  3120  rmo3  3123  csbco  3136  csbcow  3137  sbnfc2  3187  csbabg  3188  cbvralcsf  3189  cbvrexcsf  3190  cbvreucsf  3191  dfss  3213  dfss2f  3217  ss2ab  3294  dfdif3  3316  difeqri  3326  ddifstab  3338  raldifb  3346  uneqri  3348  ssequn2  3379  unss  3380  rexun  3386  ralunb  3387  elin2  3394  ineqri  3399  dfss1  3410  dfss5  3411  dfss4st  3439  ssddif  3440  difin  3443  indif  3449  difundi  3458  indifdir  3462  symdifxor  3472  inrab2  3479  rabun2  3485  reuun2  3489  0el  3516  rabeq0  3523  abeq0  3524  disjr  3543  disj1  3544  undif4  3556  uneqdifeqim  3579  r19.2m  3580  r19.3rm  3582  r19.9rmv  3585  raaan  3599  pwss  3669  dfpr2  3689  rexdifpr  3698  ralsnsg  3707  ralsns  3708  eltpg  3715  eldiftp  3716  ralprg  3721  rexprg  3722  raltpg  3723  rextpg  3724  snprc  3735  rabrsndc  3740  euabsn2  3741  eusn  3746  eldifsn  3801  ssdifsn  3802  rexdifsn  3806  eqsnm  3839  tpss  3842  snsssn  3845  prel12  3855  preqsn  3859  oprcl  3887  pwtpss  3891  eluniab  3906  elunirab  3907  unipr  3908  dfnfc2  3912  uniun  3913  uniin  3914  uni0b  3919  unissb  3924  elintab  3940  elintrab  3941  ssintab  3946  ssintrab  3952  intun  3960  intpr  3961  elrint  3969  iuncom4  3978  iuneq2  3987  dfiun2g  4003  ssiinf  4021  iundif2ss  4037  elriin  4042  iunxiun  4053  pwssb  4057  elpwpw  4058  iunpwss  4063  dfdisj2  4067  disjiun  4084  cbvopab1  4163  dftr5  4191  trint  4203  inex1  4224  inuni  4246  repizf2lem  4253  unidif0  4259  axpweq  4263  bnd2  4265  exmid01  4290  zfpair2  4302  exss  4321  elop  4325  opm  4328  otth  4336  copsex4g  4341  opeqsn  4347  opelopabsbALT  4355  brabga  4360  opelopabaf  4370  iunopab  4378  pwunss  4382  pocl  4402  frirrg  4449  elsuci  4502  elsucg  4503  sucel  4509  unisucg  4513  uniuni  4550  reusv3  4559  iunpw  4579  setindel  4638  elirr  4641  en2lp  4654  ordpwsucss  4667  zfregfr  4674  tfi  4682  peano2  4695  peano5  4698  elxp  4744  opelxp  4757  brxp  4758  rabxp  4765  opthprc  4779  brab2a  4781  opeliunxp  4783  xpundi  4784  xpundir  4785  elvvv  4791  brinxp  4796  brab2ga  4803  0xp  4808  ssrel2  4818  eqrelrel  4829  reliun  4850  reluni  4852  raliunxp  4873  rexiunxp  4874  ralxpf  4878  rexxpf  4879  iunxpf  4880  relop  4882  elco  4898  elcnv  4909  elcnv2  4910  dmin  4941  dmuni  4943  dmopab  4944  dmi  4948  dmmrnm  4953  rnopab  4981  elrnmpt1  4985  rncoeq  5008  resiexg  5060  restidsing  5071  dfima2  5080  dfima3  5081  elima2  5084  elima3  5085  imai  5094  elimasn  5105  epini  5109  dfse2  5111  cotr  5120  issref  5121  intasym  5123  asymref  5124  cnvopab  5140  cnvi  5143  cnvdif  5145  imainss  5154  rnxpid  5173  dfrel2  5189  dfrel3  5196  dmsnm  5204  rnsnm  5205  relsn2m  5209  dmsnopg  5210  cnvcnvsn  5215  elxp4  5226  elxp5  5227  cnvresima  5228  mptpreima  5232  dfco2  5238  coundi  5240  coundir  5241  imaco  5244  coiun  5248  coi1  5254  relssdmrn  5259  relrelss  5265  unixpm  5274  ressn  5279  cnviinm  5280  cnvpom  5281  cnvsom  5282  cbviota  5293  iotass  5306  eliota  5316  dffun2  5338  dffun4  5339  dffun7  5355  dffun8  5356  dffun9  5357  funopab  5363  funun  5373  funcnvsn  5377  fntpg  5388  funcnv2  5392  funcnv  5393  fun2cnv  5396  fncnv  5398  fun11  5399  fununi  5400  imadiflem  5411  imadif  5412  imainlem  5413  funimaexglem  5415  fnunsn  5441  fnres  5451  fnopabg  5458  mptfng  5460  mptun  5466  fun  5510  fcnvres  5522  dff12  5544  f1cnvcnv  5556  funforn  5569  dff1o2  5591  dff1o5  5595  f1orn  5596  resdif  5608  ffoss  5619  f11o  5620  f1o00  5623  fo00  5624  elfv  5640  fv3  5665  nfvres  5678  eqfnfv3  5749  fneqeql  5758  unpreima  5775  respreima  5778  dffo3  5797  dffo5  5799  f1ompt  5801  ffnfvf  5809  fmptco  5816  funopdmsn  5837  ftpg  5841  fnressn  5843  idref  5902  abrexco  5905  dff13  5914  dff13f  5916  fliftel  5939  isoini  5964  eusvobj2  6009  acexmidlema  6014  acexmidlemb  6015  acexmidlemph  6016  acexmidlem2  6020  oprabid  6055  brabvv  6072  dfoprab2  6073  eqoprab2b  6084  dmoprab  6107  rnoprab  6109  eloprabga  6113  mpomptx  6117  resoprab  6122  ffnov  6130  elrnmpo  6140  ralrnmpo  6141  rexrnmpo  6142  ovid  6143  ovi3  6164  ov6g  6165  foov  6174  opabex3d  6288  opabex3  6289  abexssex  6292  oprabex3  6296  oprabrexex2  6297  fmpo  6371  xporderlem  6401  f1od2  6405  mpoxopovel  6412  brtpos2  6422  dmtpos  6427  tpostpos  6435  tpossym  6447  tposoprab  6451  dfsmo2  6458  tfrlem7  6488  tfrlem9  6490  tfr1onlemaccex  6519  tfrcllemaccex  6532  tfrcldm  6534  frecabex  6569  el1o  6610  dif1o  6611  dfer2  6708  brdifun  6734  eqerlem  6738  qsid  6774  iinerm  6781  riinerm  6782  erinxp  6783  brecop  6799  eroveu  6800  erovlem  6801  ecopovsym  6805  mapval2  6852  mapsn  6864  elixp  6879  ixpeq2  6886  ixpin  6897  ixpiinm  6898  mptelixpg  6908  ixpsnf1o  6910  domen  6927  isfi  6939  en1  6978  modom2  7000  xpsnen  7010  xpcomco  7015  xpassen  7019  ssenen  7042  nneneq  7048  snnen2oprc  7051  ac6sfi  7092  exmidpw  7105  exmidpweq  7106  pw1dc1  7111  eldju  7272  djur  7273  eldju2ndl  7276  eldju2ndr  7277  finomni  7344  nninfwlporlemd  7376  nninfwlpoimlemg  7379  acfun  7427  pw1nel3  7454  sucpw1nel3  7456  ccfunen  7488  elni  7533  ltexpi  7562  enq0enq  7656  enq0ref  7658  enq0tr  7659  prarloclem3  7722  ltdfpr  7731  genpdflem  7732  genpassl  7749  genpassu  7750  nqprrnd  7768  nqprl  7776  nqpru  7777  ltexprlemopl  7826  ltexprlemopu  7828  ltexprlemdisj  7831  ltexprlemloc  7832  recexprlemdisj  7855  caucvgprprlemell  7910  caucvgprprlemelu  7911  suplocexprlemml  7941  suplocsrlemb  8031  opelcn  8051  elreal  8053  elreal2  8055  peano1nnnn  8077  axicn  8088  axaddf  8093  axmulf  8094  axprecex  8105  axpre-ltirr  8107  axpre-mulgt0  8112  axcaucvglemres  8124  axpre-suploc  8127  xrlenlt  8249  ltxrlt  8250  inelr  8769  reapcotr  8783  1nn  9159  elnnne0  9421  un0addcl  9440  un0mulcl  9441  elnnz  9494  elznn0nn  9498  elznn0  9499  elznn  9500  elz2  9556  zapne  9559  3halfnz  9582  prime  9584  raluz2  9818  rexuz2  9820  supinfneg  9834  infsupneg  9835  eluz2b2  9842  eluz2b3  9843  ublbneg  9852  elq  9861  qreccl  9881  elpq  9888  ralrp  9915  rexrp  9916  rpnegap  9926  ltxr  10015  xrnemnf  10017  xrltso  10036  icc0r  10166  divelunit  10242  fzprval  10322  fztpval  10323  elfz1b  10330  fz01or  10351  4fvwrd4  10380  fzolb  10394  fzolb2  10395  elfzo3  10404  fzouzsplit  10421  elfzo0z  10429  fzo0m  10437  fzind2  10491  ioo0  10525  ico0  10527  ioc0  10528  uzennn  10704  seq3f1olemp  10783  iswrd  11124  caucvgre  11564  cvg1nlemcau  11567  resqrexlemex  11608  climeu  11879  fsum2dlemstep  12018  expcnv  12088  prodsnf  12176  fprod2dlemstep  12206  divides  12373  m1exp1  12485  divalgb  12509  bitsval2  12528  bitsmod  12540  bitscmp  12542  bezoutlemnewy  12590  bezoutlemmain  12592  bezoutlemex  12595  dfgcd2  12608  nnwosdc  12633  lcmgcdlem  12672  isprm2  12712  isprm3  12713  isprm4  12714  isprm5  12737  sqrt2irr  12757  oddpwdc  12769  pythagtriplem19  12878  pythagtrip  12879  pceu  12891  dvdsprmpweqnn  12932  4sqlem2  12985  4sqlem12  12998  dec5dvds2  13009  ennnfoneleminc  13055  ennnfonelemex  13058  ennnfonelemr  13067  ctiunct  13084  infpn2  13100  xpsfrnel  13450  xpsfrnel2  13452  gsum0g  13502  ismnd  13525  dfgrp2e  13634  dfgrp3me  13706  isnsg2  13813  eqger  13834  isabl2  13904  imasabl  13946  isrhm  14196  isrim  14207  isnzr2  14222  lss1d  14421  istps  14785  istps2  14786  isbasis2g  14798  tgval2  14804  txuni2  15009  tx1cn  15022  tx2cn  15023  uptx  15027  txdis1cn  15031  blres  15187  xmeterval  15188  xmeter  15189  isxms2  15205  isms2  15207  metrest  15259  qtopbasss  15274  dedekindicclemicc  15385  limcdifap  15415  plyrecj  15516  pilem1  15532  sincosq1lem  15578  mpodvdsmulf1o  15743  gausslemma2dlem1a  15816  gausslemma2dlem4  15822  lgsquadlem1  15835  lgsquadlem2  15836  2lgslem1b  15847  2sqlem1  15872  upgrex  15983  griedg0ssusgr  16131  clwwlkn1loopb  16300  clwwlknon2x  16315  decidr  16453  bdcuni  16531  bdcriota  16538  bdinex1  16554  bj-zfpair2  16565  bj-axun2  16570  bj-ssom  16591  ss1oel2o  16646  nninfsellemdc  16675  nninfsellemsuc  16677  nninfsellemqall  16680  trirec0xor  16716  iswomni0  16723