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  686  mt2bi  688  orbi12i  769  or42  777  pm5.53  807  orddi  825  anddi  826  pm2.1dc  842  dcim  846  notnotrdc  848  dcnnOLD  854  rbaib  926  rbaibr  927  pm4.43  955  orbididc  959  pm5.75  968  ifptru  995  ifpfal  996  3orass  1005  3anass  1006  3ancomb  1010  3anan32  1013  3anan12  1014  anandi3  1015  anandi3r  1016  xordc  1434  falbitru  1459  19.26-2  1528  19.26-3an  1529  alrot3  1531  albiim  1533  2albiim  1534  19.27h  1606  19.27  1607  19.28h  1608  19.28  1609  nfalt  1624  aaanh  1632  aaan  1633  alinexa  1649  19.21-2  1713  nf2  1714  19.44  1728  19.45  1729  exrot3  1736  exrot4  1737  eeor  1741  sbcof2  1856  sbid2h  1895  19.23vv  1930  sbnv  1935  sblimv  1941  pm11.53  1942  19.41vv  1950  19.41vvv  1951  19.41vvvv  1952  exdistrv  1957  19.42vv  1958  19.42vvv  1959  19.42vvvv  1960  4exdistr  1963  cbvex4v  1981  eean  1982  sbn  2003  sbim  2004  sbor  2005  sban  2006  sbrim  2007  sblim  2008  sbbi  2010  sblbis  2011  sbrbis  2012  sbrbif  2013  sbco2d  2017  sbco2vd  2018  sbnf2  2032  2sb5  2034  2sb6  2035  sbcom2v  2036  sbcom2v2  2037  sbcom2  2038  sb6a  2039  2sb5rf  2040  2sb6rf  2041  sbalyz  2050  sbal  2051  sbal1yz  2052  sbex  2055  sbalv  2056  sbco4lem  2057  exsb  2059  2exsb  2060  eujust  2079  euf  2082  cbveu  2101  mor  2120  eu2  2122  mo4f  2138  eu4  2140  2exeu  2170  2eu4  2171  exists1  2174  abid  2217  eleq12i  2297  abeq2  2338  abeq2i  2340  clabel  2356  abid2f  2398  sbabel  2399  neeq12i  2417  neanior  2487  ralnex  2518  dfrex2dc  2521  ralinexa  2557  nfraldya  2565  nfrexdya  2566  r3al  2574  r19.26-2  2660  ralbiim  2665  ralnex2  2670  r19.43  2689  ralcomf  2692  rexcomf  2693  ralrot3  2696  rexrot4  2698  reean  2700  3reeanv  2702  rabbi  2709  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvral2vw  2776  cbvrex2vw  2777  cbvral2v  2778  cbvrex2v  2779  cbvral3v  2780  cbvralsv  2781  cbvrexsv  2782  sbralie  2783  rabeq2i  2797  issetf  2808  2gencl  2834  3gencl  2835  ceqsex2  2842  ceqsex3v  2844  ceqsex6v  2846  ceqsex8v  2847  gencbvex  2848  gencbval  2850  spc2gv  2895  eqvincf  2929  ceqsrex2v  2936  clel5  2941  elrab2  2963  ralab  2964  ralrab  2965  rexab  2966  rexrab  2967  ralab2  2968  rexab2  2970  eueq3dc  2978  morex  2988  euind  2991  reu2  2992  reu6  2993  rmo4  2997  reu4  2998  reu7  2999  rmo3f  3001  rmo4f  3002  rmoim  3005  2reuswapdc  3008  reuind  3009  2rmorex  3010  sbcco  3051  sbccomlem  3104  sbccom  3105  ra5  3119  rmo3  3122  csbco  3135  csbcow  3136  sbnfc2  3186  csbabg  3187  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  dfss  3212  dfss2f  3216  ss2ab  3293  dfdif3  3315  difeqri  3325  ddifstab  3337  raldifb  3345  uneqri  3347  ssequn2  3378  unss  3379  rexun  3385  ralunb  3386  elin2  3393  ineqri  3398  dfss1  3409  dfss5  3410  dfss4st  3438  ssddif  3439  difin  3442  indif  3448  difundi  3457  indifdir  3461  symdifxor  3471  inrab2  3478  rabun2  3484  reuun2  3488  0el  3515  rabeq0  3522  abeq0  3523  disjr  3542  disj1  3543  undif4  3555  uneqdifeqim  3578  r19.2m  3579  r19.3rm  3581  r19.9rmv  3584  raaan  3598  pwss  3666  dfpr2  3686  rexdifpr  3695  ralsnsg  3704  ralsns  3705  eltpg  3712  eldiftp  3713  ralprg  3718  rexprg  3719  raltpg  3720  rextpg  3721  snprc  3732  rabrsndc  3737  euabsn2  3738  eusn  3743  eldifsn  3798  ssdifsn  3799  rexdifsn  3803  eqsnm  3836  tpss  3839  snsssn  3842  prel12  3852  preqsn  3856  oprcl  3884  pwtpss  3888  eluniab  3903  elunirab  3904  unipr  3905  dfnfc2  3909  uniun  3910  uniin  3911  uni0b  3916  unissb  3921  elintab  3937  elintrab  3938  ssintab  3943  ssintrab  3949  intun  3957  intpr  3958  elrint  3966  iuncom4  3975  iuneq2  3984  dfiun2g  4000  ssiinf  4018  iundif2ss  4034  elriin  4039  iunxiun  4050  pwssb  4054  elpwpw  4055  iunpwss  4060  dfdisj2  4064  disjiun  4081  cbvopab1  4160  dftr5  4188  trint  4200  inex1  4221  inuni  4243  repizf2lem  4249  unidif0  4255  axpweq  4259  bnd2  4261  exmid01  4286  zfpair2  4298  exss  4317  elop  4321  opm  4324  otth  4332  copsex4g  4337  opeqsn  4343  opelopabsbALT  4351  brabga  4356  opelopabaf  4366  iunopab  4374  pwunss  4378  pocl  4398  frirrg  4445  elsuci  4498  elsucg  4499  sucel  4505  unisucg  4509  uniuni  4546  reusv3  4555  iunpw  4575  setindel  4634  elirr  4637  en2lp  4650  ordpwsucss  4663  zfregfr  4670  tfi  4678  peano2  4691  peano5  4694  elxp  4740  opelxp  4753  brxp  4754  rabxp  4761  opthprc  4775  brab2a  4777  opeliunxp  4779  xpundi  4780  xpundir  4781  elvvv  4787  brinxp  4792  brab2ga  4799  0xp  4804  ssrel2  4814  eqrelrel  4825  reliun  4846  reluni  4848  raliunxp  4869  rexiunxp  4870  ralxpf  4874  rexxpf  4875  iunxpf  4876  relop  4878  elco  4894  elcnv  4905  elcnv2  4906  dmin  4937  dmuni  4939  dmopab  4940  dmi  4944  dmmrnm  4949  rnopab  4977  elrnmpt1  4981  rncoeq  5004  resiexg  5056  restidsing  5067  dfima2  5076  dfima3  5077  elima2  5080  elima3  5081  imai  5090  elimasn  5101  epini  5105  dfse2  5107  cotr  5116  issref  5117  intasym  5119  asymref  5120  cnvopab  5136  cnvi  5139  cnvdif  5141  imainss  5150  rnxpid  5169  dfrel2  5185  dfrel3  5192  dmsnm  5200  rnsnm  5201  relsn2m  5205  dmsnopg  5206  cnvcnvsn  5211  elxp4  5222  elxp5  5223  cnvresima  5224  mptpreima  5228  dfco2  5234  coundi  5236  coundir  5237  imaco  5240  coiun  5244  coi1  5250  relssdmrn  5255  relrelss  5261  unixpm  5270  ressn  5275  cnviinm  5276  cnvpom  5277  cnvsom  5278  cbviota  5289  iotass  5302  eliota  5312  dffun2  5334  dffun4  5335  dffun7  5351  dffun8  5352  dffun9  5353  funopab  5359  funun  5368  funcnvsn  5372  fntpg  5383  funcnv2  5387  funcnv  5388  fun2cnv  5391  fncnv  5393  fun11  5394  fununi  5395  imadiflem  5406  imadif  5407  imainlem  5408  funimaexglem  5410  fnunsn  5436  fnres  5446  fnopabg  5453  mptfng  5455  mptun  5461  fun  5505  fcnvres  5517  dff12  5538  f1cnvcnv  5550  funforn  5563  dff1o2  5585  dff1o5  5589  f1orn  5590  resdif  5602  ffoss  5612  f11o  5613  f1o00  5616  fo00  5617  elfv  5633  fv3  5658  nfvres  5671  eqfnfv3  5742  fneqeql  5751  unpreima  5768  respreima  5771  dffo3  5790  dffo5  5792  f1ompt  5794  ffnfvf  5802  fmptco  5809  funopdmsn  5829  ftpg  5833  fnressn  5835  idref  5892  abrexco  5895  dff13  5904  dff13f  5906  fliftel  5929  isoini  5954  eusvobj2  5999  acexmidlema  6004  acexmidlemb  6005  acexmidlemph  6006  acexmidlem2  6010  oprabid  6045  brabvv  6062  dfoprab2  6063  eqoprab2b  6074  dmoprab  6097  rnoprab  6099  eloprabga  6103  mpomptx  6107  resoprab  6112  ffnov  6120  elrnmpo  6130  ralrnmpo  6131  rexrnmpo  6132  ovid  6133  ovi3  6154  ov6g  6155  foov  6164  opabex3d  6278  opabex3  6279  abexssex  6282  oprabex3  6286  oprabrexex2  6287  fmpo  6361  xporderlem  6391  f1od2  6395  mpoxopovel  6402  brtpos2  6412  dmtpos  6417  tpostpos  6425  tpossym  6437  tposoprab  6441  dfsmo2  6448  tfrlem7  6478  tfrlem9  6480  tfr1onlemaccex  6509  tfrcllemaccex  6522  tfrcldm  6524  frecabex  6559  el1o  6600  dif1o  6601  dfer2  6698  brdifun  6724  eqerlem  6728  qsid  6764  iinerm  6771  riinerm  6772  erinxp  6773  brecop  6789  eroveu  6790  erovlem  6791  ecopovsym  6795  mapval2  6842  mapsn  6854  elixp  6869  ixpeq2  6876  ixpin  6887  ixpiinm  6888  mptelixpg  6898  ixpsnf1o  6900  domen  6917  isfi  6929  en1  6968  modom2  6990  xpsnen  7000  xpcomco  7005  xpassen  7009  ssenen  7032  nneneq  7038  snnen2oprc  7041  ac6sfi  7080  exmidpw  7093  exmidpweq  7094  pw1dc1  7099  eldju  7258  djur  7259  eldju2ndl  7262  eldju2ndr  7263  finomni  7330  nninfwlporlemd  7362  nninfwlpoimlemg  7365  acfun  7412  pw1nel3  7439  sucpw1nel3  7441  ccfunen  7473  elni  7518  ltexpi  7547  enq0enq  7641  enq0ref  7643  enq0tr  7644  prarloclem3  7707  ltdfpr  7716  genpdflem  7717  genpassl  7734  genpassu  7735  nqprrnd  7753  nqprl  7761  nqpru  7762  ltexprlemopl  7811  ltexprlemopu  7813  ltexprlemdisj  7816  ltexprlemloc  7817  recexprlemdisj  7840  caucvgprprlemell  7895  caucvgprprlemelu  7896  suplocexprlemml  7926  suplocsrlemb  8016  opelcn  8036  elreal  8038  elreal2  8040  peano1nnnn  8062  axicn  8073  axaddf  8078  axmulf  8079  axprecex  8090  axpre-ltirr  8092  axpre-mulgt0  8097  axcaucvglemres  8109  axpre-suploc  8112  xrlenlt  8234  ltxrlt  8235  inelr  8754  reapcotr  8768  1nn  9144  elnnne0  9406  un0addcl  9425  un0mulcl  9426  elnnz  9479  elznn0nn  9483  elznn0  9484  elznn  9485  elz2  9541  zapne  9544  3halfnz  9567  prime  9569  raluz2  9803  rexuz2  9805  supinfneg  9819  infsupneg  9820  eluz2b2  9827  eluz2b3  9828  ublbneg  9837  elq  9846  qreccl  9866  elpq  9873  ralrp  9900  rexrp  9901  rpnegap  9911  ltxr  10000  xrnemnf  10002  xrltso  10021  icc0r  10151  divelunit  10227  fzprval  10307  fztpval  10308  elfz1b  10315  fz01or  10336  4fvwrd4  10365  fzolb  10379  fzolb2  10380  elfzo3  10389  fzouzsplit  10406  elfzo0z  10413  fzo0m  10421  fzind2  10475  ioo0  10509  ico0  10511  ioc0  10512  uzennn  10688  seq3f1olemp  10767  iswrd  11105  caucvgre  11532  cvg1nlemcau  11535  resqrexlemex  11576  climeu  11847  fsum2dlemstep  11985  expcnv  12055  prodsnf  12143  fprod2dlemstep  12173  divides  12340  m1exp1  12452  divalgb  12476  bitsval2  12495  bitsmod  12507  bitscmp  12509  bezoutlemnewy  12557  bezoutlemmain  12559  bezoutlemex  12562  dfgcd2  12575  nnwosdc  12600  lcmgcdlem  12639  isprm2  12679  isprm3  12680  isprm4  12681  isprm5  12704  sqrt2irr  12724  oddpwdc  12736  pythagtriplem19  12845  pythagtrip  12846  pceu  12858  dvdsprmpweqnn  12899  4sqlem2  12952  4sqlem12  12965  dec5dvds2  12976  ennnfoneleminc  13022  ennnfonelemex  13025  ennnfonelemr  13034  ctiunct  13051  infpn2  13067  xpsfrnel  13417  xpsfrnel2  13419  gsum0g  13469  ismnd  13492  dfgrp2e  13601  dfgrp3me  13673  isnsg2  13780  eqger  13801  isabl2  13871  imasabl  13913  isrhm  14162  isrim  14173  isnzr2  14188  lss1d  14387  istps  14746  istps2  14747  isbasis2g  14759  tgval2  14765  txuni2  14970  tx1cn  14983  tx2cn  14984  uptx  14988  txdis1cn  14992  blres  15148  xmeterval  15149  xmeter  15150  isxms2  15166  isms2  15168  metrest  15220  qtopbasss  15235  dedekindicclemicc  15346  limcdifap  15376  plyrecj  15477  pilem1  15493  sincosq1lem  15539  mpodvdsmulf1o  15704  gausslemma2dlem1a  15777  gausslemma2dlem4  15783  lgsquadlem1  15796  lgsquadlem2  15797  2lgslem1b  15808  2sqlem1  15833  upgrex  15944  griedg0ssusgr  16090  clwwlkn1loopb  16215  clwwlknon2x  16230  decidr  16328  bdcuni  16407  bdcriota  16414  bdinex1  16430  bj-zfpair2  16441  bj-axun2  16446  bj-ssom  16467  ss1oel2o  16522  nninfsellemdc  16548  nninfsellemsuc  16550  nninfsellemqall  16553  trirec0xor  16585  iswomni0  16591