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  1480  19.26-3an  1481  alrot3  1483  albiim  1485  2albiim  1486  19.27h  1558  19.27  1559  19.28h  1560  19.28  1561  nfalt  1576  aaanh  1584  aaan  1585  alinexa  1601  19.21-2  1665  nf2  1666  19.44  1680  19.45  1681  exrot3  1688  exrot4  1689  eeor  1693  sbcof2  1808  sbid2h  1847  19.23vv  1882  sbnv  1886  sblimv  1892  pm11.53  1893  19.41vv  1901  19.41vvv  1902  19.41vvvv  1903  exdistrv  1908  19.42vv  1909  19.42vvv  1910  19.42vvvv  1911  4exdistr  1914  cbvex4v  1928  eean  1929  sbn  1950  sbim  1951  sbor  1952  sban  1953  sbrim  1954  sblim  1955  sbbi  1957  sblbis  1958  sbrbis  1959  sbrbif  1960  sbco2d  1964  sbco2vd  1965  sbnf2  1979  2sb5  1981  2sb6  1982  sbcom2v  1983  sbcom2v2  1984  sbcom2  1985  sb6a  1986  2sb5rf  1987  2sb6rf  1988  sbalyz  1997  sbal  1998  sbal1yz  1999  sbex  2002  sbalv  2003  sbco4lem  2004  exsb  2006  2exsb  2007  eujust  2026  euf  2029  cbveu  2048  mor  2066  eu2  2068  mo4f  2084  eu4  2086  2exeu  2116  2eu4  2117  exists1  2120  abid  2163  eleq12i  2243  abeq2  2284  abeq2i  2286  clabel  2302  abid2f  2343  sbabel  2344  neeq12i  2362  neanior  2432  ralnex  2463  dfrex2dc  2466  ralinexa  2502  nfraldya  2510  nfrexdya  2511  r3al  2519  r19.26-2  2604  ralbiim  2609  ralnex2  2614  r19.43  2633  ralcomf  2636  rexcomf  2637  rexrot4  2641  reean  2643  3reeanv  2645  rabbi  2652  cbvralf  2694  cbvrexf  2695  cbvreu  2699  cbvral2vw  2712  cbvrex2vw  2713  cbvral2v  2714  cbvrex2v  2715  cbvral3v  2716  cbvralsv  2717  cbvrexsv  2718  sbralie  2719  rabeq2i  2732  issetf  2742  2gencl  2768  3gencl  2769  ceqsex2  2775  ceqsex3v  2777  ceqsex6v  2779  ceqsex8v  2780  gencbvex  2781  gencbval  2783  spc2gv  2826  eqvincf  2860  ceqsrex2v  2867  clel5  2872  elrab2  2894  ralab  2895  ralrab  2896  rexab  2897  rexrab  2898  ralab2  2899  rexab2  2901  eueq3dc  2909  morex  2919  euind  2922  reu2  2923  reu6  2924  rmo4  2928  reu4  2929  reu7  2930  rmo3f  2932  rmo4f  2933  rmoim  2936  2reuswapdc  2939  reuind  2940  2rmorex  2941  sbcco  2982  sbccomlem  3035  sbccom  3036  ra5  3049  rmo3  3052  csbco  3065  csbcow  3066  sbnfc2  3115  csbabg  3116  cbvralcsf  3117  cbvrexcsf  3118  cbvreucsf  3119  dfss  3141  dfss2f  3144  ss2ab  3221  dfdif3  3243  difeqri  3253  ddifstab  3265  raldifb  3273  uneqri  3275  ssequn2  3306  unss  3307  rexun  3313  ralunb  3314  elin2  3321  ineqri  3326  dfss1  3337  dfss5  3338  dfss4st  3366  ssddif  3367  difin  3370  indif  3376  difundi  3385  indifdir  3389  symdifxor  3399  inrab2  3406  rabun2  3412  reuun2  3416  0el  3443  rabeq0  3450  abeq0  3451  disjr  3470  disj1  3471  undif4  3483  uneqdifeqim  3506  r19.2m  3507  r19.3rm  3509  r19.9rmv  3512  raaan  3527  pwss  3588  dfpr2  3608  rexdifpr  3617  ralsnsg  3626  ralsns  3627  eltpg  3634  eldiftp  3635  ralprg  3640  rexprg  3641  raltpg  3642  rextpg  3643  snprc  3654  rabrsndc  3657  euabsn2  3658  eusn  3663  eldifsn  3716  ssdifsn  3717  rexdifsn  3721  eqsnm  3751  tpss  3754  snsssn  3757  prel12  3767  preqsn  3771  oprcl  3798  pwtpss  3802  eluniab  3817  elunirab  3818  unipr  3819  dfnfc2  3823  uniun  3824  uniin  3825  uni0b  3830  unissb  3835  elintab  3851  elintrab  3852  ssintab  3857  ssintrab  3863  intun  3871  intpr  3872  elrint  3880  iuncom4  3889  iuneq2  3898  dfiun2g  3914  ssiinf  3931  iundif2ss  3947  elriin  3952  iunxiun  3963  pwssb  3967  elpwpw  3968  iunpwss  3973  dfdisj2  3977  disjiun  3993  cbvopab1  4071  dftr5  4099  trint  4111  inex1  4132  inuni  4150  repizf2lem  4156  unidif0  4162  axpweq  4166  bnd2  4168  exmid01  4193  zfpair2  4204  exss  4221  elop  4225  opm  4228  otth  4236  copsex4g  4241  opeqsn  4246  opelopabsbALT  4253  brabga  4258  opelopabaf  4267  iunopab  4275  pwunss  4277  pocl  4297  frirrg  4344  elsuci  4397  elsucg  4398  sucel  4404  unisucg  4408  uniuni  4445  reusv3  4454  iunpw  4474  setindel  4531  elirr  4534  en2lp  4547  ordpwsucss  4560  zfregfr  4567  tfi  4575  peano2  4588  peano5  4591  elxp  4637  opelxp  4650  brxp  4651  rabxp  4657  opthprc  4671  brab2a  4673  opeliunxp  4675  xpundi  4676  xpundir  4677  elvvv  4683  brinxp  4688  brab2ga  4695  0xp  4700  ssrel2  4710  eqrelrel  4721  reliun  4741  reluni  4743  raliunxp  4761  rexiunxp  4762  ralxpf  4766  rexxpf  4767  iunxpf  4768  relop  4770  elco  4786  elcnv  4797  elcnv2  4798  dmin  4828  dmuni  4830  dmopab  4831  dmi  4835  dmmrnm  4839  rnopab  4867  elrnmpt1  4871  rncoeq  4893  resiexg  4945  restidsing  4956  dfima2  4965  dfima3  4966  elima2  4969  elima3  4970  imai  4977  elimasn  4988  epini  4992  dfse2  4994  cotr  5002  issref  5003  intasym  5005  asymref  5006  cnvopab  5022  cnvi  5025  cnvdif  5027  imainss  5036  rnxpid  5055  dfrel2  5071  dfrel3  5078  dmsnm  5086  rnsnm  5087  relsn2m  5091  dmsnopg  5092  cnvcnvsn  5097  elxp4  5108  elxp5  5109  cnvresima  5110  mptpreima  5114  dfco2  5120  coundi  5122  coundir  5123  imaco  5126  coiun  5130  coi1  5136  relssdmrn  5141  relrelss  5147  unixpm  5156  ressn  5161  cnviinm  5162  cnvpom  5163  cnvsom  5164  cbviota  5175  iotass  5187  eliota  5196  dffun2  5218  dffun4  5219  dffun7  5235  dffun8  5236  dffun9  5237  funopab  5243  funun  5252  funcnvsn  5253  fntpg  5264  funcnv2  5268  funcnv  5269  fun2cnv  5272  fncnv  5274  fun11  5275  fununi  5276  imadiflem  5287  imadif  5288  imainlem  5289  funimaexglem  5291  fnunsn  5315  fnres  5324  fnopabg  5331  mptfng  5333  mptun  5339  fun  5380  fcnvres  5391  dff12  5412  f1cnvcnv  5424  funforn  5437  dff1o2  5458  dff1o5  5462  f1orn  5463  resdif  5475  ffoss  5485  f11o  5486  f1o00  5488  fo00  5489  elfv  5505  fv3  5530  nfvres  5540  eqfnfv3  5607  fneqeql  5616  unpreima  5633  respreima  5636  dffo3  5655  dffo5  5657  f1ompt  5659  ffnfvf  5667  fmptco  5674  ftpg  5692  fnressn  5694  idref  5748  abrexco  5750  dff13  5759  dff13f  5761  fliftel  5784  isoini  5809  eusvobj2  5851  acexmidlema  5856  acexmidlemb  5857  acexmidlemph  5858  acexmidlem2  5862  oprabid  5897  brabvv  5911  dfoprab2  5912  eqoprab2b  5923  dmoprab  5946  rnoprab  5948  eloprabga  5952  mpomptx  5956  resoprab  5961  ffnov  5969  elrnmpo  5978  ralrnmpo  5979  rexrnmpo  5980  ovid  5981  ovi3  6001  ov6g  6002  foov  6011  opabex3d  6112  opabex3  6113  abexssex  6116  oprabex3  6120  oprabrexex2  6121  fmpo  6192  xporderlem  6222  f1od2  6226  mpoxopovel  6232  brtpos2  6242  dmtpos  6247  tpostpos  6255  tpossym  6267  tposoprab  6271  dfsmo2  6278  tfrlem7  6308  tfrlem9  6310  tfr1onlemaccex  6339  tfrcllemaccex  6352  tfrcldm  6354  frecabex  6389  el1o  6428  dif1o  6429  dfer2  6526  brdifun  6552  eqerlem  6556  qsid  6590  iinerm  6597  riinerm  6598  erinxp  6599  brecop  6615  eroveu  6616  erovlem  6617  ecopovsym  6621  mapval2  6668  mapsn  6680  elixp  6695  ixpeq2  6702  ixpin  6713  ixpiinm  6714  mptelixpg  6724  ixpsnf1o  6726  domen  6741  isfi  6751  en1  6789  xpsnen  6811  xpcomco  6816  xpassen  6820  ssenen  6841  nneneq  6847  snnen2oprc  6850  ac6sfi  6888  exmidpw  6898  exmidpweq  6899  pw1dc1  6903  eldju  7057  djur  7058  eldju2ndl  7061  eldju2ndr  7062  finomni  7128  nninfwlporlemd  7160  nninfwlpoimlemg  7163  acfun  7196  pw1nel3  7220  sucpw1nel3  7222  ccfunen  7238  elni  7282  ltexpi  7311  enq0enq  7405  enq0ref  7407  enq0tr  7408  prarloclem3  7471  ltdfpr  7480  genpdflem  7481  genpassl  7498  genpassu  7499  nqprrnd  7517  nqprl  7525  nqpru  7526  ltexprlemopl  7575  ltexprlemopu  7577  ltexprlemdisj  7580  ltexprlemloc  7581  recexprlemdisj  7604  caucvgprprlemell  7659  caucvgprprlemelu  7660  suplocexprlemml  7690  suplocsrlemb  7780  opelcn  7800  elreal  7802  elreal2  7804  peano1nnnn  7826  axicn  7837  axaddf  7842  axmulf  7843  axprecex  7854  axpre-ltirr  7856  axpre-mulgt0  7861  axcaucvglemres  7873  axpre-suploc  7876  xrlenlt  7996  ltxrlt  7997  inelr  8515  reapcotr  8529  1nn  8903  elnnne0  9163  un0addcl  9182  un0mulcl  9183  elnnz  9236  elznn0nn  9240  elznn0  9241  elznn  9242  elz2  9297  zapne  9300  3halfnz  9323  prime  9325  raluz2  9552  rexuz2  9554  supinfneg  9568  infsupneg  9569  eluz2b2  9576  eluz2b3  9577  ublbneg  9586  elq  9595  qreccl  9615  elpq  9621  ralrp  9646  rexrp  9647  rpnegap  9657  ltxr  9746  xrnemnf  9748  xrltso  9767  icc0r  9897  divelunit  9973  fzprval  10052  fztpval  10053  elfz1b  10060  fz01or  10081  4fvwrd4  10110  fzolb  10123  fzolb2  10124  elfzo3  10133  fzouzsplit  10149  elfzo0z  10154  fzo0m  10161  fzind2  10209  ioo0  10230  ico0  10232  ioc0  10233  uzennn  10406  seq3f1olemp  10472  caucvgre  10958  cvg1nlemcau  10961  resqrexlemex  11002  climeu  11272  fsum2dlemstep  11410  expcnv  11480  prodsnf  11568  fprod2dlemstep  11598  divides  11764  m1exp1  11873  divalgb  11897  bezoutlemnewy  11964  bezoutlemmain  11966  bezoutlemex  11969  dfgcd2  11982  nnwosdc  12007  lcmgcdlem  12044  isprm2  12084  isprm3  12085  isprm4  12086  isprm5  12109  sqrt2irr  12129  oddpwdc  12141  pythagtriplem19  12249  pythagtrip  12250  pceu  12262  dvdsprmpweqnn  12302  4sqlem2  12354  ennnfoneleminc  12379  ennnfonelemex  12382  ennnfonelemr  12391  ctiunct  12408  infpn2  12424  ismnd  12686  dfgrp2e  12765  dfgrp3me  12831  isabl2  12896  istps  13101  istps2  13102  isbasis2g  13114  tgval2  13122  txuni2  13327  tx1cn  13340  tx2cn  13341  uptx  13345  txdis1cn  13349  blres  13505  xmeterval  13506  xmeter  13507  isxms2  13523  isms2  13525  metrest  13577  qtopbasss  13592  dedekindicclemicc  13681  limcdifap  13702  pilem1  13771  sincosq1lem  13817  2sqlem1  14021  decidr  14108  bdcuni  14188  bdcriota  14195  bdinex1  14211  bj-zfpair2  14222  bj-axun2  14227  bj-ssom  14248  ss1oel2o  14303  nninfsellemdc  14320  nninfsellemsuc  14322  nninfsellemqall  14325  trirec0xor  14354  iswomni0  14360