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  683  mt2bi  685  orbi12i  765  or42  773  pm5.53  803  orddi  821  anddi  822  pm2.1dc  838  dcim  842  notnotrdc  844  dcnnOLD  850  rbaib  922  rbaibr  923  pm4.43  951  orbididc  955  pm5.75  964  3orass  983  3anass  984  3ancomb  988  3anan32  991  3anan12  992  anandi3  993  anandi3r  994  xordc  1403  falbitru  1428  19.26-2  1496  19.26-3an  1497  alrot3  1499  albiim  1501  2albiim  1502  19.27h  1574  19.27  1575  19.28h  1576  19.28  1577  nfalt  1592  aaanh  1600  aaan  1601  alinexa  1617  19.21-2  1681  nf2  1682  19.44  1696  19.45  1697  exrot3  1704  exrot4  1705  eeor  1709  sbcof2  1824  sbid2h  1863  19.23vv  1898  sbnv  1903  sblimv  1909  pm11.53  1910  19.41vv  1918  19.41vvv  1919  19.41vvvv  1920  exdistrv  1925  19.42vv  1926  19.42vvv  1927  19.42vvvv  1928  4exdistr  1931  cbvex4v  1949  eean  1950  sbn  1971  sbim  1972  sbor  1973  sban  1974  sbrim  1975  sblim  1976  sbbi  1978  sblbis  1979  sbrbis  1980  sbrbif  1981  sbco2d  1985  sbco2vd  1986  sbnf2  2000  2sb5  2002  2sb6  2003  sbcom2v  2004  sbcom2v2  2005  sbcom2  2006  sb6a  2007  2sb5rf  2008  2sb6rf  2009  sbalyz  2018  sbal  2019  sbal1yz  2020  sbex  2023  sbalv  2024  sbco4lem  2025  exsb  2027  2exsb  2028  eujust  2047  euf  2050  cbveu  2069  mor  2087  eu2  2089  mo4f  2105  eu4  2107  2exeu  2137  2eu4  2138  exists1  2141  abid  2184  eleq12i  2264  abeq2  2305  abeq2i  2307  clabel  2323  abid2f  2365  sbabel  2366  neeq12i  2384  neanior  2454  ralnex  2485  dfrex2dc  2488  ralinexa  2524  nfraldya  2532  nfrexdya  2533  r3al  2541  r19.26-2  2626  ralbiim  2631  ralnex2  2636  r19.43  2655  ralcomf  2658  rexcomf  2659  ralrot3  2662  rexrot4  2664  reean  2666  3reeanv  2668  rabbi  2675  cbvralf  2721  cbvrexf  2722  cbvreu  2727  cbvral2vw  2740  cbvrex2vw  2741  cbvral2v  2742  cbvrex2v  2743  cbvral3v  2744  cbvralsv  2745  cbvrexsv  2746  sbralie  2747  rabeq2i  2760  issetf  2770  2gencl  2796  3gencl  2797  ceqsex2  2804  ceqsex3v  2806  ceqsex6v  2808  ceqsex8v  2809  gencbvex  2810  gencbval  2812  spc2gv  2855  eqvincf  2889  ceqsrex2v  2896  clel5  2901  elrab2  2923  ralab  2924  ralrab  2925  rexab  2926  rexrab  2927  ralab2  2928  rexab2  2930  eueq3dc  2938  morex  2948  euind  2951  reu2  2952  reu6  2953  rmo4  2957  reu4  2958  reu7  2959  rmo3f  2961  rmo4f  2962  rmoim  2965  2reuswapdc  2968  reuind  2969  2rmorex  2970  sbcco  3011  sbccomlem  3064  sbccom  3065  ra5  3078  rmo3  3081  csbco  3094  csbcow  3095  sbnfc2  3145  csbabg  3146  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  dfss  3171  dfss2f  3174  ss2ab  3251  dfdif3  3273  difeqri  3283  ddifstab  3295  raldifb  3303  uneqri  3305  ssequn2  3336  unss  3337  rexun  3343  ralunb  3344  elin2  3351  ineqri  3356  dfss1  3367  dfss5  3368  dfss4st  3396  ssddif  3397  difin  3400  indif  3406  difundi  3415  indifdir  3419  symdifxor  3429  inrab2  3436  rabun2  3442  reuun2  3446  0el  3473  rabeq0  3480  abeq0  3481  disjr  3500  disj1  3501  undif4  3513  uneqdifeqim  3536  r19.2m  3537  r19.3rm  3539  r19.9rmv  3542  raaan  3556  pwss  3621  dfpr2  3641  rexdifpr  3650  ralsnsg  3659  ralsns  3660  eltpg  3667  eldiftp  3668  ralprg  3673  rexprg  3674  raltpg  3675  rextpg  3676  snprc  3687  rabrsndc  3690  euabsn2  3691  eusn  3696  eldifsn  3749  ssdifsn  3750  rexdifsn  3754  eqsnm  3785  tpss  3788  snsssn  3791  prel12  3801  preqsn  3805  oprcl  3832  pwtpss  3836  eluniab  3851  elunirab  3852  unipr  3853  dfnfc2  3857  uniun  3858  uniin  3859  uni0b  3864  unissb  3869  elintab  3885  elintrab  3886  ssintab  3891  ssintrab  3897  intun  3905  intpr  3906  elrint  3914  iuncom4  3923  iuneq2  3932  dfiun2g  3948  ssiinf  3966  iundif2ss  3982  elriin  3987  iunxiun  3998  pwssb  4002  elpwpw  4003  iunpwss  4008  dfdisj2  4012  disjiun  4028  cbvopab1  4106  dftr5  4134  trint  4146  inex1  4167  inuni  4188  repizf2lem  4194  unidif0  4200  axpweq  4204  bnd2  4206  exmid01  4231  zfpair2  4243  exss  4260  elop  4264  opm  4267  otth  4275  copsex4g  4280  opeqsn  4285  opelopabsbALT  4293  brabga  4298  opelopabaf  4308  iunopab  4316  pwunss  4318  pocl  4338  frirrg  4385  elsuci  4438  elsucg  4439  sucel  4445  unisucg  4449  uniuni  4486  reusv3  4495  iunpw  4515  setindel  4574  elirr  4577  en2lp  4590  ordpwsucss  4603  zfregfr  4610  tfi  4618  peano2  4631  peano5  4634  elxp  4680  opelxp  4693  brxp  4694  rabxp  4700  opthprc  4714  brab2a  4716  opeliunxp  4718  xpundi  4719  xpundir  4720  elvvv  4726  brinxp  4731  brab2ga  4738  0xp  4743  ssrel2  4753  eqrelrel  4764  reliun  4784  reluni  4786  raliunxp  4807  rexiunxp  4808  ralxpf  4812  rexxpf  4813  iunxpf  4814  relop  4816  elco  4832  elcnv  4843  elcnv2  4844  dmin  4874  dmuni  4876  dmopab  4877  dmi  4881  dmmrnm  4885  rnopab  4913  elrnmpt1  4917  rncoeq  4939  resiexg  4991  restidsing  5002  dfima2  5011  dfima3  5012  elima2  5015  elima3  5016  imai  5025  elimasn  5036  epini  5040  dfse2  5042  cotr  5051  issref  5052  intasym  5054  asymref  5055  cnvopab  5071  cnvi  5074  cnvdif  5076  imainss  5085  rnxpid  5104  dfrel2  5120  dfrel3  5127  dmsnm  5135  rnsnm  5136  relsn2m  5140  dmsnopg  5141  cnvcnvsn  5146  elxp4  5157  elxp5  5158  cnvresima  5159  mptpreima  5163  dfco2  5169  coundi  5171  coundir  5172  imaco  5175  coiun  5179  coi1  5185  relssdmrn  5190  relrelss  5196  unixpm  5205  ressn  5210  cnviinm  5211  cnvpom  5212  cnvsom  5213  cbviota  5224  iotass  5236  eliota  5246  dffun2  5268  dffun4  5269  dffun7  5285  dffun8  5286  dffun9  5287  funopab  5293  funun  5302  funcnvsn  5303  fntpg  5314  funcnv2  5318  funcnv  5319  fun2cnv  5322  fncnv  5324  fun11  5325  fununi  5326  imadiflem  5337  imadif  5338  imainlem  5339  funimaexglem  5341  fnunsn  5365  fnres  5374  fnopabg  5381  mptfng  5383  mptun  5389  fun  5430  fcnvres  5441  dff12  5462  f1cnvcnv  5474  funforn  5487  dff1o2  5509  dff1o5  5513  f1orn  5514  resdif  5526  ffoss  5536  f11o  5537  f1o00  5539  fo00  5540  elfv  5556  fv3  5581  nfvres  5592  eqfnfv3  5661  fneqeql  5670  unpreima  5687  respreima  5690  dffo3  5709  dffo5  5711  f1ompt  5713  ffnfvf  5721  fmptco  5728  ftpg  5746  fnressn  5748  idref  5803  abrexco  5806  dff13  5815  dff13f  5817  fliftel  5840  isoini  5865  eusvobj2  5908  acexmidlema  5913  acexmidlemb  5914  acexmidlemph  5915  acexmidlem2  5919  oprabid  5954  brabvv  5968  dfoprab2  5969  eqoprab2b  5980  dmoprab  6003  rnoprab  6005  eloprabga  6009  mpomptx  6013  resoprab  6018  ffnov  6026  elrnmpo  6036  ralrnmpo  6037  rexrnmpo  6038  ovid  6039  ovi3  6060  ov6g  6061  foov  6070  opabex3d  6178  opabex3  6179  abexssex  6182  oprabex3  6186  oprabrexex2  6187  fmpo  6259  xporderlem  6289  f1od2  6293  mpoxopovel  6299  brtpos2  6309  dmtpos  6314  tpostpos  6322  tpossym  6334  tposoprab  6338  dfsmo2  6345  tfrlem7  6375  tfrlem9  6377  tfr1onlemaccex  6406  tfrcllemaccex  6419  tfrcldm  6421  frecabex  6456  el1o  6495  dif1o  6496  dfer2  6593  brdifun  6619  eqerlem  6623  qsid  6659  iinerm  6666  riinerm  6667  erinxp  6668  brecop  6684  eroveu  6685  erovlem  6686  ecopovsym  6690  mapval2  6737  mapsn  6749  elixp  6764  ixpeq2  6771  ixpin  6782  ixpiinm  6783  mptelixpg  6793  ixpsnf1o  6795  domen  6810  isfi  6820  en1  6858  xpsnen  6880  xpcomco  6885  xpassen  6889  ssenen  6912  nneneq  6918  snnen2oprc  6921  ac6sfi  6959  exmidpw  6969  exmidpweq  6970  pw1dc1  6975  eldju  7134  djur  7135  eldju2ndl  7138  eldju2ndr  7139  finomni  7206  nninfwlporlemd  7238  nninfwlpoimlemg  7241  acfun  7274  pw1nel3  7298  sucpw1nel3  7300  ccfunen  7331  elni  7375  ltexpi  7404  enq0enq  7498  enq0ref  7500  enq0tr  7501  prarloclem3  7564  ltdfpr  7573  genpdflem  7574  genpassl  7591  genpassu  7592  nqprrnd  7610  nqprl  7618  nqpru  7619  ltexprlemopl  7668  ltexprlemopu  7670  ltexprlemdisj  7673  ltexprlemloc  7674  recexprlemdisj  7697  caucvgprprlemell  7752  caucvgprprlemelu  7753  suplocexprlemml  7783  suplocsrlemb  7873  opelcn  7893  elreal  7895  elreal2  7897  peano1nnnn  7919  axicn  7930  axaddf  7935  axmulf  7936  axprecex  7947  axpre-ltirr  7949  axpre-mulgt0  7954  axcaucvglemres  7966  axpre-suploc  7969  xrlenlt  8091  ltxrlt  8092  inelr  8611  reapcotr  8625  1nn  9001  elnnne0  9263  un0addcl  9282  un0mulcl  9283  elnnz  9336  elznn0nn  9340  elznn0  9341  elznn  9342  elz2  9397  zapne  9400  3halfnz  9423  prime  9425  raluz2  9653  rexuz2  9655  supinfneg  9669  infsupneg  9670  eluz2b2  9677  eluz2b3  9678  ublbneg  9687  elq  9696  qreccl  9716  elpq  9723  ralrp  9750  rexrp  9751  rpnegap  9761  ltxr  9850  xrnemnf  9852  xrltso  9871  icc0r  10001  divelunit  10077  fzprval  10157  fztpval  10158  elfz1b  10165  fz01or  10186  4fvwrd4  10215  fzolb  10229  fzolb2  10230  elfzo3  10239  fzouzsplit  10255  elfzo0z  10260  fzo0m  10267  fzind2  10315  ioo0  10349  ico0  10351  ioc0  10352  uzennn  10528  seq3f1olemp  10607  iswrd  10937  caucvgre  11146  cvg1nlemcau  11149  resqrexlemex  11190  climeu  11461  fsum2dlemstep  11599  expcnv  11669  prodsnf  11757  fprod2dlemstep  11787  divides  11954  m1exp1  12066  divalgb  12090  bitsval2  12109  bezoutlemnewy  12163  bezoutlemmain  12165  bezoutlemex  12168  dfgcd2  12181  nnwosdc  12206  lcmgcdlem  12245  isprm2  12285  isprm3  12286  isprm4  12287  isprm5  12310  sqrt2irr  12330  oddpwdc  12342  pythagtriplem19  12451  pythagtrip  12452  pceu  12464  dvdsprmpweqnn  12505  4sqlem2  12558  4sqlem12  12571  dec5dvds2  12582  ennnfoneleminc  12628  ennnfonelemex  12631  ennnfonelemr  12640  ctiunct  12657  infpn2  12673  xpsfrnel  12987  xpsfrnel2  12989  gsum0g  13039  ismnd  13060  dfgrp2e  13160  dfgrp3me  13232  isnsg2  13333  eqger  13354  isabl2  13424  imasabl  13466  isrhm  13714  isrim  13725  isnzr2  13740  lss1d  13939  istps  14268  istps2  14269  isbasis2g  14281  tgval2  14287  txuni2  14492  tx1cn  14505  tx2cn  14506  uptx  14510  txdis1cn  14514  blres  14670  xmeterval  14671  xmeter  14672  isxms2  14688  isms2  14690  metrest  14742  qtopbasss  14757  dedekindicclemicc  14868  limcdifap  14898  plyrecj  14999  pilem1  15015  sincosq1lem  15061  mpodvdsmulf1o  15226  gausslemma2dlem1a  15299  gausslemma2dlem4  15305  lgsquadlem1  15318  lgsquadlem2  15319  2lgslem1b  15330  2sqlem1  15355  decidr  15442  bdcuni  15522  bdcriota  15529  bdinex1  15545  bj-zfpair2  15556  bj-axun2  15561  bj-ssom  15582  ss1oel2o  15638  nninfsellemdc  15654  nninfsellemsuc  15656  nninfsellemqall  15659  trirec0xor  15689  iswomni0  15695