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  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  ralrot3  2642  rexrot4  2644  reean  2646  3reeanv  2648  rabbi  2655  cbvralf  2697  cbvrexf  2698  cbvreu  2703  cbvral2vw  2716  cbvrex2vw  2717  cbvral2v  2718  cbvrex2v  2719  cbvral3v  2720  cbvralsv  2721  cbvrexsv  2722  sbralie  2723  rabeq2i  2736  issetf  2746  2gencl  2772  3gencl  2773  ceqsex2  2779  ceqsex3v  2781  ceqsex6v  2783  ceqsex8v  2784  gencbvex  2785  gencbval  2787  spc2gv  2830  eqvincf  2864  ceqsrex2v  2871  clel5  2876  elrab2  2898  ralab  2899  ralrab  2900  rexab  2901  rexrab  2902  ralab2  2903  rexab2  2905  eueq3dc  2913  morex  2923  euind  2926  reu2  2927  reu6  2928  rmo4  2932  reu4  2933  reu7  2934  rmo3f  2936  rmo4f  2937  rmoim  2940  2reuswapdc  2943  reuind  2944  2rmorex  2945  sbcco  2986  sbccomlem  3039  sbccom  3040  ra5  3053  rmo3  3056  csbco  3069  csbcow  3070  sbnfc2  3119  csbabg  3120  cbvralcsf  3121  cbvrexcsf  3122  cbvreucsf  3123  dfss  3145  dfss2f  3148  ss2ab  3225  dfdif3  3247  difeqri  3257  ddifstab  3269  raldifb  3277  uneqri  3279  ssequn2  3310  unss  3311  rexun  3317  ralunb  3318  elin2  3325  ineqri  3330  dfss1  3341  dfss5  3342  dfss4st  3370  ssddif  3371  difin  3374  indif  3380  difundi  3389  indifdir  3393  symdifxor  3403  inrab2  3410  rabun2  3416  reuun2  3420  0el  3447  rabeq0  3454  abeq0  3455  disjr  3474  disj1  3475  undif4  3487  uneqdifeqim  3510  r19.2m  3511  r19.3rm  3513  r19.9rmv  3516  raaan  3531  pwss  3593  dfpr2  3613  rexdifpr  3622  ralsnsg  3631  ralsns  3632  eltpg  3639  eldiftp  3640  ralprg  3645  rexprg  3646  raltpg  3647  rextpg  3648  snprc  3659  rabrsndc  3662  euabsn2  3663  eusn  3668  eldifsn  3721  ssdifsn  3722  rexdifsn  3726  eqsnm  3757  tpss  3760  snsssn  3763  prel12  3773  preqsn  3777  oprcl  3804  pwtpss  3808  eluniab  3823  elunirab  3824  unipr  3825  dfnfc2  3829  uniun  3830  uniin  3831  uni0b  3836  unissb  3841  elintab  3857  elintrab  3858  ssintab  3863  ssintrab  3869  intun  3877  intpr  3878  elrint  3886  iuncom4  3895  iuneq2  3904  dfiun2g  3920  ssiinf  3938  iundif2ss  3954  elriin  3959  iunxiun  3970  pwssb  3974  elpwpw  3975  iunpwss  3980  dfdisj2  3984  disjiun  4000  cbvopab1  4078  dftr5  4106  trint  4118  inex1  4139  inuni  4157  repizf2lem  4163  unidif0  4169  axpweq  4173  bnd2  4175  exmid01  4200  zfpair2  4212  exss  4229  elop  4233  opm  4236  otth  4244  copsex4g  4249  opeqsn  4254  opelopabsbALT  4261  brabga  4266  opelopabaf  4275  iunopab  4283  pwunss  4285  pocl  4305  frirrg  4352  elsuci  4405  elsucg  4406  sucel  4412  unisucg  4416  uniuni  4453  reusv3  4462  iunpw  4482  setindel  4539  elirr  4542  en2lp  4555  ordpwsucss  4568  zfregfr  4575  tfi  4583  peano2  4596  peano5  4599  elxp  4645  opelxp  4658  brxp  4659  rabxp  4665  opthprc  4679  brab2a  4681  opeliunxp  4683  xpundi  4684  xpundir  4685  elvvv  4691  brinxp  4696  brab2ga  4703  0xp  4708  ssrel2  4718  eqrelrel  4729  reliun  4749  reluni  4751  raliunxp  4770  rexiunxp  4771  ralxpf  4775  rexxpf  4776  iunxpf  4777  relop  4779  elco  4795  elcnv  4806  elcnv2  4807  dmin  4837  dmuni  4839  dmopab  4840  dmi  4844  dmmrnm  4848  rnopab  4876  elrnmpt1  4880  rncoeq  4902  resiexg  4954  restidsing  4965  dfima2  4974  dfima3  4975  elima2  4978  elima3  4979  imai  4986  elimasn  4997  epini  5001  dfse2  5003  cotr  5012  issref  5013  intasym  5015  asymref  5016  cnvopab  5032  cnvi  5035  cnvdif  5037  imainss  5046  rnxpid  5065  dfrel2  5081  dfrel3  5088  dmsnm  5096  rnsnm  5097  relsn2m  5101  dmsnopg  5102  cnvcnvsn  5107  elxp4  5118  elxp5  5119  cnvresima  5120  mptpreima  5124  dfco2  5130  coundi  5132  coundir  5133  imaco  5136  coiun  5140  coi1  5146  relssdmrn  5151  relrelss  5157  unixpm  5166  ressn  5171  cnviinm  5172  cnvpom  5173  cnvsom  5174  cbviota  5185  iotass  5197  eliota  5206  dffun2  5228  dffun4  5229  dffun7  5245  dffun8  5246  dffun9  5247  funopab  5253  funun  5262  funcnvsn  5263  fntpg  5274  funcnv2  5278  funcnv  5279  fun2cnv  5282  fncnv  5284  fun11  5285  fununi  5286  imadiflem  5297  imadif  5298  imainlem  5299  funimaexglem  5301  fnunsn  5325  fnres  5334  fnopabg  5341  mptfng  5343  mptun  5349  fun  5390  fcnvres  5401  dff12  5422  f1cnvcnv  5434  funforn  5447  dff1o2  5468  dff1o5  5472  f1orn  5473  resdif  5485  ffoss  5495  f11o  5496  f1o00  5498  fo00  5499  elfv  5515  fv3  5540  nfvres  5550  eqfnfv3  5617  fneqeql  5626  unpreima  5643  respreima  5646  dffo3  5665  dffo5  5667  f1ompt  5669  ffnfvf  5677  fmptco  5684  ftpg  5702  fnressn  5704  idref  5759  abrexco  5762  dff13  5771  dff13f  5773  fliftel  5796  isoini  5821  eusvobj2  5863  acexmidlema  5868  acexmidlemb  5869  acexmidlemph  5870  acexmidlem2  5874  oprabid  5909  brabvv  5923  dfoprab2  5924  eqoprab2b  5935  dmoprab  5958  rnoprab  5960  eloprabga  5964  mpomptx  5968  resoprab  5973  ffnov  5981  elrnmpo  5990  ralrnmpo  5991  rexrnmpo  5992  ovid  5993  ovi3  6013  ov6g  6014  foov  6023  opabex3d  6124  opabex3  6125  abexssex  6128  oprabex3  6132  oprabrexex2  6133  fmpo  6204  xporderlem  6234  f1od2  6238  mpoxopovel  6244  brtpos2  6254  dmtpos  6259  tpostpos  6267  tpossym  6279  tposoprab  6283  dfsmo2  6290  tfrlem7  6320  tfrlem9  6322  tfr1onlemaccex  6351  tfrcllemaccex  6364  tfrcldm  6366  frecabex  6401  el1o  6440  dif1o  6441  dfer2  6538  brdifun  6564  eqerlem  6568  qsid  6602  iinerm  6609  riinerm  6610  erinxp  6611  brecop  6627  eroveu  6628  erovlem  6629  ecopovsym  6633  mapval2  6680  mapsn  6692  elixp  6707  ixpeq2  6714  ixpin  6725  ixpiinm  6726  mptelixpg  6736  ixpsnf1o  6738  domen  6753  isfi  6763  en1  6801  xpsnen  6823  xpcomco  6828  xpassen  6832  ssenen  6853  nneneq  6859  snnen2oprc  6862  ac6sfi  6900  exmidpw  6910  exmidpweq  6911  pw1dc1  6915  eldju  7069  djur  7070  eldju2ndl  7073  eldju2ndr  7074  finomni  7140  nninfwlporlemd  7172  nninfwlpoimlemg  7175  acfun  7208  pw1nel3  7232  sucpw1nel3  7234  ccfunen  7265  elni  7309  ltexpi  7338  enq0enq  7432  enq0ref  7434  enq0tr  7435  prarloclem3  7498  ltdfpr  7507  genpdflem  7508  genpassl  7525  genpassu  7526  nqprrnd  7544  nqprl  7552  nqpru  7553  ltexprlemopl  7602  ltexprlemopu  7604  ltexprlemdisj  7607  ltexprlemloc  7608  recexprlemdisj  7631  caucvgprprlemell  7686  caucvgprprlemelu  7687  suplocexprlemml  7717  suplocsrlemb  7807  opelcn  7827  elreal  7829  elreal2  7831  peano1nnnn  7853  axicn  7864  axaddf  7869  axmulf  7870  axprecex  7881  axpre-ltirr  7883  axpre-mulgt0  7888  axcaucvglemres  7900  axpre-suploc  7903  xrlenlt  8024  ltxrlt  8025  inelr  8543  reapcotr  8557  1nn  8932  elnnne0  9192  un0addcl  9211  un0mulcl  9212  elnnz  9265  elznn0nn  9269  elznn0  9270  elznn  9271  elz2  9326  zapne  9329  3halfnz  9352  prime  9354  raluz2  9581  rexuz2  9583  supinfneg  9597  infsupneg  9598  eluz2b2  9605  eluz2b3  9606  ublbneg  9615  elq  9624  qreccl  9644  elpq  9650  ralrp  9677  rexrp  9678  rpnegap  9688  ltxr  9777  xrnemnf  9779  xrltso  9798  icc0r  9928  divelunit  10004  fzprval  10084  fztpval  10085  elfz1b  10092  fz01or  10113  4fvwrd4  10142  fzolb  10155  fzolb2  10156  elfzo3  10165  fzouzsplit  10181  elfzo0z  10186  fzo0m  10193  fzind2  10241  ioo0  10262  ico0  10264  ioc0  10265  uzennn  10438  seq3f1olemp  10504  caucvgre  10992  cvg1nlemcau  10995  resqrexlemex  11036  climeu  11306  fsum2dlemstep  11444  expcnv  11514  prodsnf  11602  fprod2dlemstep  11632  divides  11798  m1exp1  11908  divalgb  11932  bezoutlemnewy  11999  bezoutlemmain  12001  bezoutlemex  12004  dfgcd2  12017  nnwosdc  12042  lcmgcdlem  12079  isprm2  12119  isprm3  12120  isprm4  12121  isprm5  12144  sqrt2irr  12164  oddpwdc  12176  pythagtriplem19  12284  pythagtrip  12285  pceu  12297  dvdsprmpweqnn  12337  4sqlem2  12389  ennnfoneleminc  12414  ennnfonelemex  12417  ennnfonelemr  12426  ctiunct  12443  infpn2  12459  xpsfrnel  12768  xpsfrnel2  12770  ismnd  12825  dfgrp2e  12908  dfgrp3me  12975  isnsg2  13068  eqger  13088  isabl2  13102  lss1d  13475  istps  13571  istps2  13572  isbasis2g  13584  tgval2  13590  txuni2  13795  tx1cn  13808  tx2cn  13809  uptx  13813  txdis1cn  13817  blres  13973  xmeterval  13974  xmeter  13975  isxms2  13991  isms2  13993  metrest  14045  qtopbasss  14060  dedekindicclemicc  14149  limcdifap  14170  pilem1  14239  sincosq1lem  14285  2sqlem1  14500  decidr  14587  bdcuni  14667  bdcriota  14674  bdinex1  14690  bj-zfpair2  14701  bj-axun2  14706  bj-ssom  14727  ss1oel2o  14782  nninfsellemdc  14798  nninfsellemsuc  14800  nninfsellemqall  14803  trirec0xor  14832  iswomni0  14838