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  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  1715  nf2  1716  19.44  1730  19.45  1731  exrot3  1738  exrot4  1739  eeor  1743  sbcof2  1858  sbid2h  1897  19.23vv  1932  sbnv  1937  sblimv  1943  pm11.53  1944  19.41vv  1952  19.41vvv  1953  19.41vvvv  1954  exdistrv  1959  19.42vv  1960  19.42vvv  1961  19.42vvvv  1962  4exdistr  1965  cbvex4v  1983  eean  1984  sbn  2005  sbim  2006  sbor  2007  sban  2008  sbrim  2009  sblim  2010  sbbi  2012  sblbis  2013  sbrbis  2014  sbrbif  2015  sbco2d  2019  sbco2vd  2020  sbnf2  2034  2sb5  2036  2sb6  2037  sbcom2v  2038  sbcom2v2  2039  sbcom2  2040  sb6a  2041  2sb5rf  2042  2sb6rf  2043  sbalyz  2052  sbal  2053  sbal1yz  2054  sbex  2057  sbalv  2058  sbco4lem  2059  exsb  2061  2exsb  2062  eujust  2081  euf  2084  cbveu  2103  mor  2122  eu2  2124  mo4f  2140  eu4  2142  2exeu  2172  2eu4  2173  exists1  2176  abid  2219  eleq12i  2299  abeq2  2340  abeq2i  2342  clabel  2358  abid2f  2400  sbabel  2401  neeq12i  2419  neanior  2489  ralnex  2520  dfrex2dc  2523  ralinexa  2559  nfraldya  2567  nfrexdya  2568  r3al  2576  r19.26-2  2662  ralbiim  2667  ralnex2  2672  r19.43  2691  ralcomf  2694  rexcomf  2695  ralrot3  2698  rexrot4  2700  reean  2702  3reeanv  2704  rabbi  2711  cbvralf  2758  cbvrexf  2759  cbvreu  2765  cbvral2vw  2778  cbvrex2vw  2779  cbvral2v  2780  cbvrex2v  2781  cbvral3v  2782  cbvralsv  2783  cbvrexsv  2784  sbralie  2785  rabeq2i  2799  issetf  2810  2gencl  2836  3gencl  2837  ceqsex2  2844  ceqsex3v  2846  ceqsex6v  2848  ceqsex8v  2849  gencbvex  2850  gencbval  2852  spc2gv  2897  eqvincf  2931  ceqsrex2v  2938  clel5  2943  elrab2  2965  ralab  2966  ralrab  2967  rexab  2968  rexrab  2969  ralab2  2970  rexab2  2972  eueq3dc  2980  morex  2990  euind  2993  reu2  2994  reu6  2995  rmo4  2999  reu4  3000  reu7  3001  rmo3f  3003  rmo4f  3004  rmoim  3007  2reuswapdc  3010  reuind  3011  2rmorex  3012  sbcco  3053  sbccomlem  3106  sbccom  3107  ra5  3121  rmo3  3124  csbco  3137  csbcow  3138  sbnfc2  3188  csbabg  3189  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  dfss  3214  dfss2f  3218  ss2ab  3295  dfdif3  3317  difeqri  3327  ddifstab  3339  raldifb  3347  uneqri  3349  ssequn2  3380  unss  3381  rexun  3387  ralunb  3388  elin2  3395  ineqri  3400  dfss1  3411  dfss5  3412  dfss4st  3440  ssddif  3441  difin  3444  indif  3450  difundi  3459  indifdir  3463  symdifxor  3473  inrab2  3480  rabun2  3486  reuun2  3490  0el  3517  rabeq0  3524  abeq0  3525  disjr  3544  disj1  3545  undif4  3557  uneqdifeqim  3580  r19.2m  3581  r19.3rm  3583  r19.9rmv  3586  raaan  3600  pwss  3668  dfpr2  3688  rexdifpr  3697  ralsnsg  3706  ralsns  3707  eltpg  3714  eldiftp  3715  ralprg  3720  rexprg  3721  raltpg  3722  rextpg  3723  snprc  3734  rabrsndc  3739  euabsn2  3740  eusn  3745  eldifsn  3800  ssdifsn  3801  rexdifsn  3805  eqsnm  3838  tpss  3841  snsssn  3844  prel12  3854  preqsn  3858  oprcl  3886  pwtpss  3890  eluniab  3905  elunirab  3906  unipr  3907  dfnfc2  3911  uniun  3912  uniin  3913  uni0b  3918  unissb  3923  elintab  3939  elintrab  3940  ssintab  3945  ssintrab  3951  intun  3959  intpr  3960  elrint  3968  iuncom4  3977  iuneq2  3986  dfiun2g  4002  ssiinf  4020  iundif2ss  4036  elriin  4041  iunxiun  4052  pwssb  4056  elpwpw  4057  iunpwss  4062  dfdisj2  4066  disjiun  4083  cbvopab1  4162  dftr5  4190  trint  4202  inex1  4223  inuni  4245  repizf2lem  4251  unidif0  4257  axpweq  4261  bnd2  4263  exmid01  4288  zfpair2  4300  exss  4319  elop  4323  opm  4326  otth  4334  copsex4g  4339  opeqsn  4345  opelopabsbALT  4353  brabga  4358  opelopabaf  4368  iunopab  4376  pwunss  4380  pocl  4400  frirrg  4447  elsuci  4500  elsucg  4501  sucel  4507  unisucg  4511  uniuni  4548  reusv3  4557  iunpw  4577  setindel  4636  elirr  4639  en2lp  4652  ordpwsucss  4665  zfregfr  4672  tfi  4680  peano2  4693  peano5  4696  elxp  4742  opelxp  4755  brxp  4756  rabxp  4763  opthprc  4777  brab2a  4779  opeliunxp  4781  xpundi  4782  xpundir  4783  elvvv  4789  brinxp  4794  brab2ga  4801  0xp  4806  ssrel2  4816  eqrelrel  4827  reliun  4848  reluni  4850  raliunxp  4871  rexiunxp  4872  ralxpf  4876  rexxpf  4877  iunxpf  4878  relop  4880  elco  4896  elcnv  4907  elcnv2  4908  dmin  4939  dmuni  4941  dmopab  4942  dmi  4946  dmmrnm  4951  rnopab  4979  elrnmpt1  4983  rncoeq  5006  resiexg  5058  restidsing  5069  dfima2  5078  dfima3  5079  elima2  5082  elima3  5083  imai  5092  elimasn  5103  epini  5107  dfse2  5109  cotr  5118  issref  5119  intasym  5121  asymref  5122  cnvopab  5138  cnvi  5141  cnvdif  5143  imainss  5152  rnxpid  5171  dfrel2  5187  dfrel3  5194  dmsnm  5202  rnsnm  5203  relsn2m  5207  dmsnopg  5208  cnvcnvsn  5213  elxp4  5224  elxp5  5225  cnvresima  5226  mptpreima  5230  dfco2  5236  coundi  5238  coundir  5239  imaco  5242  coiun  5246  coi1  5252  relssdmrn  5257  relrelss  5263  unixpm  5272  ressn  5277  cnviinm  5278  cnvpom  5279  cnvsom  5280  cbviota  5291  iotass  5304  eliota  5314  dffun2  5336  dffun4  5337  dffun7  5353  dffun8  5354  dffun9  5355  funopab  5361  funun  5371  funcnvsn  5375  fntpg  5386  funcnv2  5390  funcnv  5391  fun2cnv  5394  fncnv  5396  fun11  5397  fununi  5398  imadiflem  5409  imadif  5410  imainlem  5411  funimaexglem  5413  fnunsn  5439  fnres  5449  fnopabg  5456  mptfng  5458  mptun  5464  fun  5508  fcnvres  5520  dff12  5541  f1cnvcnv  5553  funforn  5566  dff1o2  5588  dff1o5  5592  f1orn  5593  resdif  5605  ffoss  5616  f11o  5617  f1o00  5620  fo00  5621  elfv  5637  fv3  5662  nfvres  5675  eqfnfv3  5746  fneqeql  5755  unpreima  5772  respreima  5775  dffo3  5794  dffo5  5796  f1ompt  5798  ffnfvf  5806  fmptco  5813  funopdmsn  5833  ftpg  5837  fnressn  5839  idref  5896  abrexco  5899  dff13  5908  dff13f  5910  fliftel  5933  isoini  5958  eusvobj2  6003  acexmidlema  6008  acexmidlemb  6009  acexmidlemph  6010  acexmidlem2  6014  oprabid  6049  brabvv  6066  dfoprab2  6067  eqoprab2b  6078  dmoprab  6101  rnoprab  6103  eloprabga  6107  mpomptx  6111  resoprab  6116  ffnov  6124  elrnmpo  6134  ralrnmpo  6135  rexrnmpo  6136  ovid  6137  ovi3  6158  ov6g  6159  foov  6168  opabex3d  6282  opabex3  6283  abexssex  6286  oprabex3  6290  oprabrexex2  6291  fmpo  6365  xporderlem  6395  f1od2  6399  mpoxopovel  6406  brtpos2  6416  dmtpos  6421  tpostpos  6429  tpossym  6441  tposoprab  6445  dfsmo2  6452  tfrlem7  6482  tfrlem9  6484  tfr1onlemaccex  6513  tfrcllemaccex  6526  tfrcldm  6528  frecabex  6563  el1o  6604  dif1o  6605  dfer2  6702  brdifun  6728  eqerlem  6732  qsid  6768  iinerm  6775  riinerm  6776  erinxp  6777  brecop  6793  eroveu  6794  erovlem  6795  ecopovsym  6799  mapval2  6846  mapsn  6858  elixp  6873  ixpeq2  6880  ixpin  6891  ixpiinm  6892  mptelixpg  6902  ixpsnf1o  6904  domen  6921  isfi  6933  en1  6972  modom2  6994  xpsnen  7004  xpcomco  7009  xpassen  7013  ssenen  7036  nneneq  7042  snnen2oprc  7045  ac6sfi  7086  exmidpw  7099  exmidpweq  7100  pw1dc1  7105  eldju  7266  djur  7267  eldju2ndl  7270  eldju2ndr  7271  finomni  7338  nninfwlporlemd  7370  nninfwlpoimlemg  7373  acfun  7421  pw1nel3  7448  sucpw1nel3  7450  ccfunen  7482  elni  7527  ltexpi  7556  enq0enq  7650  enq0ref  7652  enq0tr  7653  prarloclem3  7716  ltdfpr  7725  genpdflem  7726  genpassl  7743  genpassu  7744  nqprrnd  7762  nqprl  7770  nqpru  7771  ltexprlemopl  7820  ltexprlemopu  7822  ltexprlemdisj  7825  ltexprlemloc  7826  recexprlemdisj  7849  caucvgprprlemell  7904  caucvgprprlemelu  7905  suplocexprlemml  7935  suplocsrlemb  8025  opelcn  8045  elreal  8047  elreal2  8049  peano1nnnn  8071  axicn  8082  axaddf  8087  axmulf  8088  axprecex  8099  axpre-ltirr  8101  axpre-mulgt0  8106  axcaucvglemres  8118  axpre-suploc  8121  xrlenlt  8243  ltxrlt  8244  inelr  8763  reapcotr  8777  1nn  9153  elnnne0  9415  un0addcl  9434  un0mulcl  9435  elnnz  9488  elznn0nn  9492  elznn0  9493  elznn  9494  elz2  9550  zapne  9553  3halfnz  9576  prime  9578  raluz2  9812  rexuz2  9814  supinfneg  9828  infsupneg  9829  eluz2b2  9836  eluz2b3  9837  ublbneg  9846  elq  9855  qreccl  9875  elpq  9882  ralrp  9909  rexrp  9910  rpnegap  9920  ltxr  10009  xrnemnf  10011  xrltso  10030  icc0r  10160  divelunit  10236  fzprval  10316  fztpval  10317  elfz1b  10324  fz01or  10345  4fvwrd4  10374  fzolb  10388  fzolb2  10389  elfzo3  10398  fzouzsplit  10415  elfzo0z  10422  fzo0m  10430  fzind2  10484  ioo0  10518  ico0  10520  ioc0  10521  uzennn  10697  seq3f1olemp  10776  iswrd  11114  caucvgre  11541  cvg1nlemcau  11544  resqrexlemex  11585  climeu  11856  fsum2dlemstep  11994  expcnv  12064  prodsnf  12152  fprod2dlemstep  12182  divides  12349  m1exp1  12461  divalgb  12485  bitsval2  12504  bitsmod  12516  bitscmp  12518  bezoutlemnewy  12566  bezoutlemmain  12568  bezoutlemex  12571  dfgcd2  12584  nnwosdc  12609  lcmgcdlem  12648  isprm2  12688  isprm3  12689  isprm4  12690  isprm5  12713  sqrt2irr  12733  oddpwdc  12745  pythagtriplem19  12854  pythagtrip  12855  pceu  12867  dvdsprmpweqnn  12908  4sqlem2  12961  4sqlem12  12974  dec5dvds2  12985  ennnfoneleminc  13031  ennnfonelemex  13034  ennnfonelemr  13043  ctiunct  13060  infpn2  13076  xpsfrnel  13426  xpsfrnel2  13428  gsum0g  13478  ismnd  13501  dfgrp2e  13610  dfgrp3me  13682  isnsg2  13789  eqger  13810  isabl2  13880  imasabl  13922  isrhm  14171  isrim  14182  isnzr2  14197  lss1d  14396  istps  14755  istps2  14756  isbasis2g  14768  tgval2  14774  txuni2  14979  tx1cn  14992  tx2cn  14993  uptx  14997  txdis1cn  15001  blres  15157  xmeterval  15158  xmeter  15159  isxms2  15175  isms2  15177  metrest  15229  qtopbasss  15244  dedekindicclemicc  15355  limcdifap  15385  plyrecj  15486  pilem1  15502  sincosq1lem  15548  mpodvdsmulf1o  15713  gausslemma2dlem1a  15786  gausslemma2dlem4  15792  lgsquadlem1  15805  lgsquadlem2  15806  2lgslem1b  15817  2sqlem1  15842  upgrex  15953  griedg0ssusgr  16101  clwwlkn1loopb  16270  clwwlknon2x  16285  decidr  16392  bdcuni  16471  bdcriota  16478  bdinex1  16494  bj-zfpair2  16505  bj-axun2  16510  bj-ssom  16531  ss1oel2o  16586  nninfsellemdc  16612  nninfsellemsuc  16614  nninfsellemqall  16617  trirec0xor  16649  iswomni0  16655