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  2796  issetf  2807  2gencl  2833  3gencl  2834  ceqsex2  2841  ceqsex3v  2843  ceqsex6v  2845  ceqsex8v  2846  gencbvex  2847  gencbval  2849  spc2gv  2894  eqvincf  2928  ceqsrex2v  2935  clel5  2940  elrab2  2962  ralab  2963  ralrab  2964  rexab  2965  rexrab  2966  ralab2  2967  rexab2  2969  eueq3dc  2977  morex  2987  euind  2990  reu2  2991  reu6  2992  rmo4  2996  reu4  2997  reu7  2998  rmo3f  3000  rmo4f  3001  rmoim  3004  2reuswapdc  3007  reuind  3008  2rmorex  3009  sbcco  3050  sbccomlem  3103  sbccom  3104  ra5  3118  rmo3  3121  csbco  3134  csbcow  3135  sbnfc2  3185  csbabg  3186  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  dfss  3211  dfss2f  3215  ss2ab  3292  dfdif3  3314  difeqri  3324  ddifstab  3336  raldifb  3344  uneqri  3346  ssequn2  3377  unss  3378  rexun  3384  ralunb  3385  elin2  3392  ineqri  3397  dfss1  3408  dfss5  3409  dfss4st  3437  ssddif  3438  difin  3441  indif  3447  difundi  3456  indifdir  3460  symdifxor  3470  inrab2  3477  rabun2  3483  reuun2  3487  0el  3514  rabeq0  3521  abeq0  3522  disjr  3541  disj1  3542  undif4  3554  uneqdifeqim  3577  r19.2m  3578  r19.3rm  3580  r19.9rmv  3583  raaan  3597  pwss  3665  dfpr2  3685  rexdifpr  3694  ralsnsg  3703  ralsns  3704  eltpg  3711  eldiftp  3712  ralprg  3717  rexprg  3718  raltpg  3719  rextpg  3720  snprc  3731  rabrsndc  3734  euabsn2  3735  eusn  3740  eldifsn  3794  ssdifsn  3795  rexdifsn  3799  eqsnm  3832  tpss  3835  snsssn  3838  prel12  3848  preqsn  3852  oprcl  3880  pwtpss  3884  eluniab  3899  elunirab  3900  unipr  3901  dfnfc2  3905  uniun  3906  uniin  3907  uni0b  3912  unissb  3917  elintab  3933  elintrab  3934  ssintab  3939  ssintrab  3945  intun  3953  intpr  3954  elrint  3962  iuncom4  3971  iuneq2  3980  dfiun2g  3996  ssiinf  4014  iundif2ss  4030  elriin  4035  iunxiun  4046  pwssb  4050  elpwpw  4051  iunpwss  4056  dfdisj2  4060  disjiun  4077  cbvopab1  4156  dftr5  4184  trint  4196  inex1  4217  inuni  4238  repizf2lem  4244  unidif0  4250  axpweq  4254  bnd2  4256  exmid01  4281  zfpair2  4293  exss  4312  elop  4316  opm  4319  otth  4327  copsex4g  4332  opeqsn  4338  opelopabsbALT  4346  brabga  4351  opelopabaf  4361  iunopab  4369  pwunss  4373  pocl  4393  frirrg  4440  elsuci  4493  elsucg  4494  sucel  4500  unisucg  4504  uniuni  4541  reusv3  4550  iunpw  4570  setindel  4629  elirr  4632  en2lp  4645  ordpwsucss  4658  zfregfr  4665  tfi  4673  peano2  4686  peano5  4689  elxp  4735  opelxp  4748  brxp  4749  rabxp  4755  opthprc  4769  brab2a  4771  opeliunxp  4773  xpundi  4774  xpundir  4775  elvvv  4781  brinxp  4786  brab2ga  4793  0xp  4798  ssrel2  4808  eqrelrel  4819  reliun  4839  reluni  4841  raliunxp  4862  rexiunxp  4863  ralxpf  4867  rexxpf  4868  iunxpf  4869  relop  4871  elco  4887  elcnv  4898  elcnv2  4899  dmin  4930  dmuni  4932  dmopab  4933  dmi  4937  dmmrnm  4942  rnopab  4970  elrnmpt1  4974  rncoeq  4997  resiexg  5049  restidsing  5060  dfima2  5069  dfima3  5070  elima2  5073  elima3  5074  imai  5083  elimasn  5094  epini  5098  dfse2  5100  cotr  5109  issref  5110  intasym  5112  asymref  5113  cnvopab  5129  cnvi  5132  cnvdif  5134  imainss  5143  rnxpid  5162  dfrel2  5178  dfrel3  5185  dmsnm  5193  rnsnm  5194  relsn2m  5198  dmsnopg  5199  cnvcnvsn  5204  elxp4  5215  elxp5  5216  cnvresima  5217  mptpreima  5221  dfco2  5227  coundi  5229  coundir  5230  imaco  5233  coiun  5237  coi1  5243  relssdmrn  5248  relrelss  5254  unixpm  5263  ressn  5268  cnviinm  5269  cnvpom  5270  cnvsom  5271  cbviota  5282  iotass  5295  eliota  5305  dffun2  5327  dffun4  5328  dffun7  5344  dffun8  5345  dffun9  5346  funopab  5352  funun  5361  funcnvsn  5365  fntpg  5376  funcnv2  5380  funcnv  5381  fun2cnv  5384  fncnv  5386  fun11  5387  fununi  5388  imadiflem  5399  imadif  5400  imainlem  5401  funimaexglem  5403  fnunsn  5429  fnres  5439  fnopabg  5446  mptfng  5448  mptun  5454  fun  5496  fcnvres  5508  dff12  5529  f1cnvcnv  5541  funforn  5554  dff1o2  5576  dff1o5  5580  f1orn  5581  resdif  5593  ffoss  5603  f11o  5604  f1o00  5607  fo00  5608  elfv  5624  fv3  5649  nfvres  5662  eqfnfv3  5733  fneqeql  5742  unpreima  5759  respreima  5762  dffo3  5781  dffo5  5783  f1ompt  5785  ffnfvf  5793  fmptco  5800  funopdmsn  5818  ftpg  5822  fnressn  5824  idref  5879  abrexco  5882  dff13  5891  dff13f  5893  fliftel  5916  isoini  5941  eusvobj2  5986  acexmidlema  5991  acexmidlemb  5992  acexmidlemph  5993  acexmidlem2  5997  oprabid  6032  brabvv  6049  dfoprab2  6050  eqoprab2b  6061  dmoprab  6084  rnoprab  6086  eloprabga  6090  mpomptx  6094  resoprab  6099  ffnov  6107  elrnmpo  6117  ralrnmpo  6118  rexrnmpo  6119  ovid  6120  ovi3  6141  ov6g  6142  foov  6151  opabex3d  6264  opabex3  6265  abexssex  6268  oprabex3  6272  oprabrexex2  6273  fmpo  6345  xporderlem  6375  f1od2  6379  mpoxopovel  6385  brtpos2  6395  dmtpos  6400  tpostpos  6408  tpossym  6420  tposoprab  6424  dfsmo2  6431  tfrlem7  6461  tfrlem9  6463  tfr1onlemaccex  6492  tfrcllemaccex  6505  tfrcldm  6507  frecabex  6542  el1o  6581  dif1o  6582  dfer2  6679  brdifun  6705  eqerlem  6709  qsid  6745  iinerm  6752  riinerm  6753  erinxp  6754  brecop  6770  eroveu  6771  erovlem  6772  ecopovsym  6776  mapval2  6823  mapsn  6835  elixp  6850  ixpeq2  6857  ixpin  6868  ixpiinm  6869  mptelixpg  6879  ixpsnf1o  6881  domen  6898  isfi  6910  en1  6949  xpsnen  6976  xpcomco  6981  xpassen  6985  ssenen  7008  nneneq  7014  snnen2oprc  7017  ac6sfi  7056  exmidpw  7066  exmidpweq  7067  pw1dc1  7072  eldju  7231  djur  7232  eldju2ndl  7235  eldju2ndr  7236  finomni  7303  nninfwlporlemd  7335  nninfwlpoimlemg  7338  acfun  7385  pw1nel3  7412  sucpw1nel3  7414  ccfunen  7446  elni  7491  ltexpi  7520  enq0enq  7614  enq0ref  7616  enq0tr  7617  prarloclem3  7680  ltdfpr  7689  genpdflem  7690  genpassl  7707  genpassu  7708  nqprrnd  7726  nqprl  7734  nqpru  7735  ltexprlemopl  7784  ltexprlemopu  7786  ltexprlemdisj  7789  ltexprlemloc  7790  recexprlemdisj  7813  caucvgprprlemell  7868  caucvgprprlemelu  7869  suplocexprlemml  7899  suplocsrlemb  7989  opelcn  8009  elreal  8011  elreal2  8013  peano1nnnn  8035  axicn  8046  axaddf  8051  axmulf  8052  axprecex  8063  axpre-ltirr  8065  axpre-mulgt0  8070  axcaucvglemres  8082  axpre-suploc  8085  xrlenlt  8207  ltxrlt  8208  inelr  8727  reapcotr  8741  1nn  9117  elnnne0  9379  un0addcl  9398  un0mulcl  9399  elnnz  9452  elznn0nn  9456  elznn0  9457  elznn  9458  elz2  9514  zapne  9517  3halfnz  9540  prime  9542  raluz2  9770  rexuz2  9772  supinfneg  9786  infsupneg  9787  eluz2b2  9794  eluz2b3  9795  ublbneg  9804  elq  9813  qreccl  9833  elpq  9840  ralrp  9867  rexrp  9868  rpnegap  9878  ltxr  9967  xrnemnf  9969  xrltso  9988  icc0r  10118  divelunit  10194  fzprval  10274  fztpval  10275  elfz1b  10282  fz01or  10303  4fvwrd4  10332  fzolb  10346  fzolb2  10347  elfzo3  10356  fzouzsplit  10373  elfzo0z  10380  fzo0m  10387  fzind2  10440  ioo0  10474  ico0  10476  ioc0  10477  uzennn  10653  seq3f1olemp  10732  iswrd  11068  caucvgre  11487  cvg1nlemcau  11490  resqrexlemex  11531  climeu  11802  fsum2dlemstep  11940  expcnv  12010  prodsnf  12098  fprod2dlemstep  12128  divides  12295  m1exp1  12407  divalgb  12431  bitsval2  12450  bitsmod  12462  bitscmp  12464  bezoutlemnewy  12512  bezoutlemmain  12514  bezoutlemex  12517  dfgcd2  12530  nnwosdc  12555  lcmgcdlem  12594  isprm2  12634  isprm3  12635  isprm4  12636  isprm5  12659  sqrt2irr  12679  oddpwdc  12691  pythagtriplem19  12800  pythagtrip  12801  pceu  12813  dvdsprmpweqnn  12854  4sqlem2  12907  4sqlem12  12920  dec5dvds2  12931  ennnfoneleminc  12977  ennnfonelemex  12980  ennnfonelemr  12989  ctiunct  13006  infpn2  13022  xpsfrnel  13372  xpsfrnel2  13374  gsum0g  13424  ismnd  13447  dfgrp2e  13556  dfgrp3me  13628  isnsg2  13735  eqger  13756  isabl2  13826  imasabl  13868  isrhm  14116  isrim  14127  isnzr2  14142  lss1d  14341  istps  14700  istps2  14701  isbasis2g  14713  tgval2  14719  txuni2  14924  tx1cn  14937  tx2cn  14938  uptx  14942  txdis1cn  14946  blres  15102  xmeterval  15103  xmeter  15104  isxms2  15120  isms2  15122  metrest  15174  qtopbasss  15189  dedekindicclemicc  15300  limcdifap  15330  plyrecj  15431  pilem1  15447  sincosq1lem  15493  mpodvdsmulf1o  15658  gausslemma2dlem1a  15731  gausslemma2dlem4  15737  lgsquadlem1  15750  lgsquadlem2  15751  2lgslem1b  15762  2sqlem1  15787  upgrex  15897  decidr  16118  bdcuni  16197  bdcriota  16204  bdinex1  16220  bj-zfpair2  16231  bj-axun2  16236  bj-ssom  16257  ss1oel2o  16313  nninfsellemdc  16335  nninfsellemsuc  16337  nninfsellemqall  16340  trirec0xor  16372  iswomni0  16378