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	|- ( ph <-> ps )
bitri.2	|- ( ps <-> ch )

Assertion

Ref	Expression
bitri	|- ( ph <-> ch )

Proof of Theorem bitri

Step	Hyp	Ref	Expression
1		bitri.1	. . . 4 |- ( ph <-> ps )
2	1	biimpi 120	. . 3 |- ( ph -> ps )
3		bitri.2	. . 3 |- ( ps <-> ch )
4	2, 3	sylib 122	. 2 |- ( ph -> ch )
5	3	biimpri 133	. . 3 |- ( ch -> ps )
6	5, 1	sylibr 134	. 2 |- ( ch -> ph )
7	4, 6	impbii 126	1 |- ( ph <-> ch )

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  2945  ceqsrex2v  2952  clel5  2957  elrab2  2979  ralab  2980  ralrab  2981  rexab  2982  rexrab  2983  ralab2  2984  rexab2  2986  eueq3dc  2994  morex  3004  euind  3007  reu2  3008  reu6  3009  rmo4  3013  reu4  3014  reu7  3015  rmo3f  3017  rmo4f  3018  rmoim  3021  2reuswapdc  3024  reuind  3025  2rmorex  3026  sbcco  3067  sbccomlem  3120  sbccom  3121  ra5  3135  rmo3  3138  csbco  3151  csbcow  3152  sbnfc2  3202  csbabg  3203  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  dfss  3228  dfssf  3232  dfss2f  3233  ss2ab  3310  dfdif3  3333  difeqri  3343  ddifstab  3355  raldifb  3363  uneqri  3365  ssequn2  3396  unss  3397  rexun  3403  ralunb  3404  elin2  3411  ineqri  3418  dfss1  3429  dfss5  3430  dfss4st  3458  ssddif  3459  difin  3462  indif  3468  difundi  3477  indifdir  3481  symdifxor  3491  inrab2  3498  rabun2  3504  reuun2  3508  0el  3535  rabeq0  3542  abeq0  3543  disjr  3562  disj1  3563  undif4  3575  uneqdifeqim  3599  r19.2m  3600  r19.3rm  3602  r19.9rmv  3605  raaan  3619  pwss  3693  dfpr2  3713  rexdifpr  3722  ralsnsg  3731  ralsns  3732  eltpg  3739  eldiftp  3740  ralprg  3745  rexprg  3746  raltpg  3747  rextpg  3748  snprc  3759  rabrsndc  3764  euabsn2  3765  eusn  3770  eldifsn  3825  ssdifsn  3826  rexdifsn  3830  eqsnm  3864  tpss  3867  snsssn  3870  prel12  3880  preqsn  3884  oprcl  3912  pwtpss  3916  eluniab  3931  elunirab  3932  unipr  3933  dfnfc2  3937  uniun  3938  uniin  3939  uni0b  3944  unissb  3949  elintab  3965  elintrab  3966  ssintab  3971  ssintrab  3977  intun  3985  intpr  3986  elrint  3994  iuncom4  4003  iuneq2  4012  dfiun2g  4028  ssiinf  4046  iundif2ss  4062  elriin  4067  iunxiun  4078  pwssb  4082  elpwpw  4083  iunpwss  4088  dfdisj2  4092  disjiun  4109  cbvopab1  4188  dftr5  4216  trint  4228  inex1  4249  inuni  4272  repizf2lem  4279  unidif0  4285  axpweq  4289  bnd2  4291  exmid01  4316  zfpair2  4328  exss  4348  elop  4352  opm  4355  otth  4363  copsex4g  4368  opeqsn  4374  opelopabsbALT  4382  brabga  4387  opelopabaf  4397  iunopab  4405  pwunss  4409  pocl  4429  frirrg  4476  elsuci  4529  elsucg  4530  sucel  4536  unisucg  4540  uniuni  4577  reusv3  4586  iunpw  4606  setindel  4665  elirr  4668  en2lp  4681  ordpwsucss  4694  zfregfr  4701  tfi  4709  peano2  4722  peano5  4725  elxp  4771  opelxp  4784  brxp  4785  rabxp  4792  opthprc  4806  brab2a  4808  opeliunxp  4810  xpundi  4811  xpundir  4812  elvvv  4818  brinxp  4823  brab2ga  4830  0xp  4835  ssrel2  4845  eqrelrel  4856  reliun  4878  reluni  4880  raliunxp  4901  rexiunxp  4902  ralxpf  4906  rexxpf  4907  iunxpf  4908  relop  4910  elco  4926  elcnv  4937  elcnv2  4938  dmin  4969  dmuni  4971  dmopab  4972  dmi  4976  dmmrnm  4981  rnopab  5009  elrnmpt1  5013  rncoeq  5036  resiexg  5088  restidsing  5099  dfima2  5108  dfima3  5109  elima2  5112  elima3  5113  imai  5123  elimasn  5134  epini  5138  dfse2  5140  cotr  5149  issref  5150  intasym  5152  asymref  5153  cnvopab  5169  cnvi  5172  cnvdif  5174  imainss  5183  rnxpid  5202  dfrel2  5218  dfrel3  5225  dmsnm  5233  rnsnm  5234  relsn2m  5238  dmsnopg  5239  cnvcnvsn  5244  elxp4  5255  elxp5  5256  cnvresima  5257  mptpreima  5261  dfco2  5267  coundi  5269  coundir  5270  imaco  5273  coiun  5277  coi1  5283  relssdmrn  5288  relrelss  5294  unixpm  5303  ressn  5308  cnviinm  5309  cnvpom  5310  cnvsom  5311  cbviota  5322  iotass  5335  eliota  5345  dffun2  5367  dffun4  5368  dffun7  5384  dffun8  5385  dffun9  5386  funopab  5392  funun  5402  funcnvsn  5406  fntpg  5417  funcnv2  5421  funcnv  5422  fun2cnv  5425  fncnv  5427  fun11  5428  fununi  5429  imadiflem  5440  imadif  5441  imainlem  5442  funimaexglem  5444  fnunsn  5470  fnres  5480  fnopabg  5487  mptfng  5489  mptun  5495  fun  5541  fcnvres  5555  dff12  5577  f1cnvcnv  5589  funforn  5602  dff1o2  5624  dff1o5  5628  f1orn  5629  resdif  5641  ffoss  5652  f11o  5653  f1o00  5656  fo00  5657  elfv  5673  fv3  5698  nfvres  5711  eqfnfv3  5782  fneqeql  5791  unpreima  5807  respreima  5810  dffo3  5829  dffo5  5831  f1ompt  5833  ffnfvf  5841  fmptco  5848  funopdmsn  5869  ftpg  5873  fnressn  5875  idref  5935  abrexco  5938  dff13  5947  dff13f  5949  fliftel  5972  isoini  5997  eusvobj2  6044  acexmidlema  6049  acexmidlemb  6050  acexmidlemph  6051  acexmidlem2  6055  oprabid  6090  brabvv  6107  dfoprab2  6108  eqoprab2b  6119  dmoprab  6142  rnoprab  6144  eloprabga  6148  mpomptx  6152  resoprab  6157  ffnov  6165  elrnmpo  6175  ralrnmpo  6176  rexrnmpo  6177  ovid  6178  ovi3  6199  ov6g  6200  foov  6209  opabex3d  6323  opabex3  6324  abexssex  6327  oprabex3  6335  oprabrexex2  6336  fmpo  6410  xporderlem  6440  f1od2  6444  mpoxopovel  6485  brtpos2  6495  dmtpos  6500  tpostpos  6508  tpossym  6520  tposoprab  6524  dfsmo2  6531  tfrlem7  6561  tfrlem9  6563  tfr1onlemaccex  6592  tfrcllemaccex  6605  tfrcldm  6607  frecabex  6642  el1o  6683  dif1o  6684  dfer2  6781  brdifun  6807  eqerlem  6811  qsid  6847  iinerm  6854  riinerm  6855  erinxp  6856  brecop  6872  eroveu  6873  erovlem  6874  ecopovsym  6878  mapval2  6925  mapsn  6938  elixp  6953  ixpeq2  6960  ixpin  6971  ixpiinm  6972  mptelixpg  6982  ixpsnf1o  6984  domen  7001  isfi  7013  en1  7052  modom2  7075  xpsnen  7085  xpcomco  7090  xpassen  7094  ssenen  7118  nneneq  7124  snnen2oprc  7127  ac6sfi  7168  exmidpw  7181  exmidpweq  7182  pw1dc1  7187  elfpw  7228  eldju  7372  djur  7373  eldju2ndl  7376  eldju2ndr  7377  finomni  7444  nninfwlporlemd  7476  nninfwlpoimlemg  7479  acfun  7527  pw1nel3  7554  sucpw1nel3  7556  ccfunen  7594  elni  7639  ltexpi  7668  enq0enq  7762  enq0ref  7764  enq0tr  7765  prarloclem3  7828  ltdfpr  7837  genpdflem  7838  genpassl  7855  genpassu  7856  nqprrnd  7874  nqprl  7882  nqpru  7883  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemdisj  7937  ltexprlemloc  7938  recexprlemdisj  7961  caucvgprprlemell  8016  caucvgprprlemelu  8017  suplocexprlemml  8047  suplocsrlemb  8137  opelcn  8157  elreal  8159  elreal2  8161  peano1nnnn  8183  axicn  8194  axaddf  8199  axmulf  8200  axprecex  8211  axpre-ltirr  8213  axpre-mulgt0  8218  axcaucvglemres  8230  axpre-suploc  8233  xrlenlt  8354  ltxrlt  8355  inelr  8875  reapcotr  8889  1nn  9265  elnnne0  9527  un0addcl  9546  un0mulcl  9547  elnnz  9604  elznn0nn  9608  elznn0  9609  elznn  9610  elz2  9666  zapne  9669  3halfnz  9693  prime  9695  raluz2  9929  rexuz2  9931  supinfneg  9945  infsupneg  9946  eluz2b2  9953  eluz2b3  9954  ublbneg  9963  elq  9972  qreccl  9992  elpq  9999  ralrp  10026  rexrp  10027  rpnegap  10037  ltxr  10127  xrnemnf  10129  xrltso  10148  icc0r  10278  divelunit  10354  fzprval  10438  fztpval  10439  elfz1b  10446  fz01or  10467  4fvwrd4  10496  fzolb  10510  fzolb2  10511  elfzo3  10520  fzouzsplit  10537  elfzo0z  10545  fzo0m  10553  fzind2  10607  infssfzcldc  10618  infssfzledc  10619  ioo0  10643  ico0  10645  ioc0  10646  uzennn  10822  seq3f1olemp  10901  sseqn  11228  hashfibc  11232  iswrd  11251  caucvgre  11691  cvg1nlemcau  11694  resqrexlemex  11735  climeu  12006  fsum2dlemstep  12145  expcnv  12215  prodsnf  12303  fprod2dlemstep  12333  divides  12500  m1exp1  12612  divalgb  12636  bitsval2  12655  bitsmod  12667  bitscmp  12669  bezoutlemnewy  12717  bezoutlemmain  12719  bezoutlemex  12722  dfgcd2  12735  nnwosdc  12760  lcmgcdlem  12799  isprm2  12839  isprm3  12840  isprm4  12841  isprm5  12864  sqrt2irr  12884  oddpwdc  12896  pythagtriplem19  13005  pythagtrip  13006  pceu  13018  dvdsprmpweqnn  13059  4sqlem2  13112  4sqlem12  13125  dec5dvds2  13136  ballotfilemodife  13184  ballotfilem4  13185  ennnfoneleminc  13246  ennnfonelemex  13249  ennnfonelemr  13258  ctiunct  13275  infpn2  13291  xpsfrnel  13608  xpsfrnel2  13610  gsum0g  13659  ismnd  13680  dfgrp2e  13783  dfgrp3me  13855  isnsg2  13956  eqger  13977  isabl2  14047  imasabl  14089  isrhm  14403  isrim  14414  isnzr2  14429  drngprop  14555  lss1d  14657  istps  15023  istps2  15024  isbasis2g  15036  tgval2  15042  txuni2  15247  tx1cn  15260  tx2cn  15261  uptx  15265  txdis1cn  15269  blres  15425  xmeterval  15426  xmeter  15427  isxms2  15443  isms2  15445  metrest  15497  qtopbasss  15512  dedekindicclemicc  15623  limcdifap  15653  plyrecj  15754  pilem1  15770  sincosq1lem  15816  mpodvdsmulf1o  15984  gausslemma2dlem1a  16057  gausslemma2dlem4  16063  lgsquadlem1  16076  lgsquadlem2  16077  2lgslem1b  16088  2sqlem1  16113  upgrex  16224  griedg0ssusgr  16372  clwwlkn1loopb  16541  clwwlknon2x  16556  decidr  16694  bdcuni  16772  bdcriota  16779  bdinex1  16795  bj-zfpair2  16806  bj-axun2  16811  bj-ssom  16832  ss1oel2o  16887  nninfsellemdc  16914  nninfsellemsuc  16916  nninfsellemqall  16919  trirec0xor  16955  iswomni0  16962