Theorem bitri 183

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 119	. . 3 |- ( ph -> ps )
3		bitri.2	. . 3 |- ( ps <-> ch )
4	2, 3	sylib 121	. 2 |- ( ph -> ch )
5	3	biimpri 132	. . 3 |- ( ch -> ps )
6	5, 1	sylibr 133	. 2 |- ( ch -> ph )
7	4, 6	impbii 125	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bitr2i  184  bitr3i  185  bitr4i  186  bitrd  187  3bitri  205  3bitr2i  207  3bitr3i  209  3bitr4i  211  bibi12i  228  imbi12i  238  pm4.71r  388  biadan2  452  anbi2ci  455  anbi12i  456  anbi12ci  457  pm5.3  467  an42  577  xchbinx  672  mt2bi  674  orbi12i  754  or42  762  pm5.53  792  orddi  810  anddi  811  pm2.1dc  827  dcim  831  notnotrdc  833  dcnnOLD  839  rbaib  911  rbaibr  912  pm4.43  939  orbididc  943  pm5.75  952  3orass  971  3anass  972  3ancomb  976  3anan32  979  3anan12  980  anandi3  981  anandi3r  982  xordc  1382  falbitru  1407  19.26-2  1470  19.26-3an  1471  alrot3  1473  albiim  1475  2albiim  1476  19.27h  1548  19.27  1549  19.28h  1550  19.28  1551  nfalt  1566  aaanh  1574  aaan  1575  alinexa  1591  19.21-2  1655  nf2  1656  19.44  1670  19.45  1671  exrot3  1678  exrot4  1679  eeor  1683  sbcof2  1798  sbid2h  1837  19.23vv  1872  sbnv  1876  sblimv  1882  pm11.53  1883  19.41vv  1891  19.41vvv  1892  19.41vvvv  1893  exdistrv  1898  19.42vv  1899  19.42vvv  1900  19.42vvvv  1901  4exdistr  1904  cbvex4v  1918  eean  1919  sbn  1940  sbim  1941  sbor  1942  sban  1943  sbrim  1944  sblim  1945  sbbi  1947  sblbis  1948  sbrbis  1949  sbrbif  1950  sbco2d  1954  sbco2vd  1955  sbnf2  1969  2sb5  1971  2sb6  1972  sbcom2v  1973  sbcom2v2  1974  sbcom2  1975  sb6a  1976  2sb5rf  1977  2sb6rf  1978  sbalyz  1987  sbal  1988  sbal1yz  1989  sbex  1992  sbalv  1993  sbco4lem  1994  exsb  1996  2exsb  1997  eujust  2016  euf  2019  cbveu  2038  mor  2056  eu2  2058  mo4f  2074  eu4  2076  2exeu  2106  2eu4  2107  exists1  2110  abid  2153  eleq12i  2233  abeq2  2274  abeq2i  2276  clabel  2292  abid2f  2333  sbabel  2334  neeq12i  2352  neanior  2422  ralnex  2453  dfrex2dc  2456  ralinexa  2492  nfraldya  2500  nfrexdya  2501  r3al  2509  r19.26-2  2594  ralbiim  2599  ralnex2  2604  r19.43  2623  ralcomf  2626  rexcomf  2627  rexrot4  2631  reean  2633  3reeanv  2635  rabbi  2642  cbvralf  2684  cbvrexf  2685  cbvreu  2689  cbvral2vw  2702  cbvrex2vw  2703  cbvral2v  2704  cbvrex2v  2705  cbvral3v  2706  cbvralsv  2707  cbvrexsv  2708  sbralie  2709  rabeq2i  2722  issetf  2732  2gencl  2758  3gencl  2759  ceqsex2  2765  ceqsex3v  2767  ceqsex6v  2769  ceqsex8v  2770  gencbvex  2771  gencbval  2773  spc2gv  2816  eqvincf  2850  ceqsrex2v  2857  clel5  2862  elrab2  2884  ralab  2885  ralrab  2886  rexab  2887  rexrab  2888  ralab2  2889  rexab2  2891  eueq3dc  2899  morex  2909  euind  2912  reu2  2913  reu6  2914  rmo4  2918  reu4  2919  reu7  2920  rmo3f  2922  rmo4f  2923  rmoim  2926  2reuswapdc  2929  reuind  2930  2rmorex  2931  sbcco  2971  sbccomlem  3024  sbccom  3025  ra5  3038  rmo3  3041  csbco  3054  csbcow  3055  sbnfc2  3104  csbabg  3105  cbvralcsf  3106  cbvrexcsf  3107  cbvreucsf  3108  dfss  3129  dfss2f  3132  ss2ab  3209  dfdif3  3231  difeqri  3241  ddifstab  3253  raldifb  3261  uneqri  3263  ssequn2  3294  unss  3295  rexun  3301  ralunb  3302  elin2  3309  ineqri  3314  dfss1  3325  dfss5  3326  dfss4st  3354  ssddif  3355  difin  3358  indif  3364  difundi  3373  indifdir  3377  symdifxor  3387  inrab2  3394  rabun2  3400  reuun2  3404  0el  3430  rabeq0  3437  abeq0  3438  disjr  3457  disj1  3458  undif4  3470  uneqdifeqim  3493  r19.2m  3494  r19.3rm  3496  r19.9rmv  3499  raaan  3514  pwss  3574  dfpr2  3594  rexdifpr  3603  ralsnsg  3612  ralsns  3613  eltpg  3620  eldiftp  3621  ralprg  3626  rexprg  3627  raltpg  3628  rextpg  3629  snprc  3640  rabrsndc  3643  euabsn2  3644  eusn  3649  eldifsn  3702  ssdifsn  3703  rexdifsn  3707  eqsnm  3734  tpss  3737  snsssn  3740  prel12  3750  preqsn  3754  oprcl  3781  pwtpss  3785  eluniab  3800  elunirab  3801  unipr  3802  dfnfc2  3806  uniun  3807  uniin  3808  uni0b  3813  unissb  3818  elintab  3834  elintrab  3835  ssintab  3840  ssintrab  3846  intun  3854  intpr  3855  elrint  3863  iuncom4  3872  iuneq2  3881  dfiun2g  3897  ssiinf  3914  iundif2ss  3930  elriin  3935  iunxiun  3946  pwssb  3950  elpwpw  3951  iunpwss  3956  dfdisj2  3960  disjiun  3976  cbvopab1  4054  dftr5  4082  trint  4094  inex1  4115  inuni  4133  repizf2lem  4139  unidif0  4145  axpweq  4149  bnd2  4151  exmid01  4176  zfpair2  4187  exss  4204  elop  4208  opm  4211  otth  4219  copsex4g  4224  opeqsn  4229  opelopabsbALT  4236  brabga  4241  opelopabaf  4250  iunopab  4258  pwunss  4260  pocl  4280  frirrg  4327  elsuci  4380  elsucg  4381  sucel  4387  unisucg  4391  uniuni  4428  reusv3  4437  iunpw  4457  setindel  4514  elirr  4517  en2lp  4530  ordpwsucss  4543  zfregfr  4550  tfi  4558  peano2  4571  peano5  4574  elxp  4620  opelxp  4633  brxp  4634  rabxp  4640  opthprc  4654  brab2a  4656  opeliunxp  4658  xpundi  4659  xpundir  4660  elvvv  4666  brinxp  4671  brab2ga  4678  0xp  4683  ssrel2  4693  eqrelrel  4704  reliun  4724  reluni  4726  raliunxp  4744  rexiunxp  4745  ralxpf  4749  rexxpf  4750  iunxpf  4751  relop  4753  elco  4769  elcnv  4780  elcnv2  4781  dmin  4811  dmuni  4813  dmopab  4814  dmi  4818  dmmrnm  4822  rnopab  4850  elrnmpt1  4854  rncoeq  4876  resiexg  4928  dfima2  4947  dfima3  4948  elima2  4951  elima3  4952  imai  4959  elimasn  4970  epini  4974  dfse2  4976  cotr  4984  issref  4985  intasym  4987  asymref  4988  cnvopab  5004  cnvi  5007  cnvdif  5009  imainss  5018  rnxpid  5037  dfrel2  5053  dfrel3  5060  dmsnm  5068  rnsnm  5069  relsn2m  5073  dmsnopg  5074  cnvcnvsn  5079  elxp4  5090  elxp5  5091  cnvresima  5092  mptpreima  5096  dfco2  5102  coundi  5104  coundir  5105  imaco  5108  coiun  5112  coi1  5118  relssdmrn  5123  relrelss  5129  unixpm  5138  ressn  5143  cnviinm  5144  cnvpom  5145  cnvsom  5146  cbviota  5157  iotass  5169  dffun2  5197  dffun4  5198  dffun7  5214  dffun8  5215  dffun9  5216  funopab  5222  funun  5231  funcnvsn  5232  fntpg  5243  funcnv2  5247  funcnv  5248  fun2cnv  5251  fncnv  5253  fun11  5254  fununi  5255  imadiflem  5266  imadif  5267  imainlem  5268  funimaexglem  5270  fnunsn  5294  fnres  5303  fnopabg  5310  mptfng  5312  mptun  5318  fun  5359  fcnvres  5370  dff12  5391  f1cnvcnv  5403  funforn  5416  dff1o2  5436  dff1o5  5440  f1orn  5441  resdif  5453  ffoss  5463  f11o  5464  f1o00  5466  fo00  5467  elfv  5483  fv3  5508  nfvres  5518  eqfnfv3  5584  fneqeql  5592  unpreima  5609  respreima  5612  dffo3  5631  dffo5  5633  f1ompt  5635  ffnfvf  5643  fmptco  5650  ftpg  5668  fnressn  5670  idref  5724  abrexco  5726  dff13  5735  dff13f  5737  fliftel  5760  isoini  5785  eusvobj2  5827  acexmidlema  5832  acexmidlemb  5833  acexmidlemph  5834  acexmidlem2  5838  oprabid  5870  brabvv  5884  dfoprab2  5885  eqoprab2b  5896  dmoprab  5919  rnoprab  5921  eloprabga  5925  mpomptx  5929  resoprab  5934  ffnov  5942  elrnmpo  5951  ralrnmpo  5952  rexrnmpo  5953  ovid  5954  ovi3  5974  ov6g  5975  foov  5984  opabex3d  6086  opabex3  6087  abexssex  6090  oprabex3  6094  oprabrexex2  6095  fmpo  6166  xporderlem  6195  f1od2  6199  mpoxopovel  6205  brtpos2  6215  dmtpos  6220  tpostpos  6228  tpossym  6240  tposoprab  6244  dfsmo2  6251  tfrlem7  6281  tfrlem9  6283  tfr1onlemaccex  6312  tfrcllemaccex  6325  tfrcldm  6327  frecabex  6362  el1o  6401  dif1o  6402  dfer2  6498  brdifun  6524  eqerlem  6528  qsid  6562  iinerm  6569  riinerm  6570  erinxp  6571  brecop  6587  eroveu  6588  erovlem  6589  ecopovsym  6593  mapval2  6640  mapsn  6652  elixp  6667  ixpeq2  6674  ixpin  6685  ixpiinm  6686  mptelixpg  6696  ixpsnf1o  6698  domen  6713  isfi  6723  en1  6761  xpsnen  6783  xpcomco  6788  xpassen  6792  ssenen  6813  nneneq  6819  snnen2oprc  6822  ac6sfi  6860  exmidpw  6870  exmidpweq  6871  pw1dc1  6875  eldju  7029  djur  7030  eldju2ndl  7033  eldju2ndr  7034  finomni  7100  acfun  7159  pw1nel3  7183  sucpw1nel3  7185  ccfunen  7201  elni  7245  ltexpi  7274  enq0enq  7368  enq0ref  7370  enq0tr  7371  prarloclem3  7434  ltdfpr  7443  genpdflem  7444  genpassl  7461  genpassu  7462  nqprrnd  7480  nqprl  7488  nqpru  7489  ltexprlemopl  7538  ltexprlemopu  7540  ltexprlemdisj  7543  ltexprlemloc  7544  recexprlemdisj  7567  caucvgprprlemell  7622  caucvgprprlemelu  7623  suplocexprlemml  7653  suplocsrlemb  7743  opelcn  7763  elreal  7765  elreal2  7767  peano1nnnn  7789  axicn  7800  axaddf  7805  axmulf  7806  axprecex  7817  axpre-ltirr  7819  axpre-mulgt0  7824  axcaucvglemres  7836  axpre-suploc  7839  xrlenlt  7959  ltxrlt  7960  inelr  8478  reapcotr  8492  1nn  8864  elnnne0  9124  un0addcl  9143  un0mulcl  9144  elnnz  9197  elznn0nn  9201  elznn0  9202  elznn  9203  elz2  9258  zapne  9261  3halfnz  9284  prime  9286  raluz2  9513  rexuz2  9515  supinfneg  9529  infsupneg  9530  eluz2b2  9537  eluz2b3  9538  ublbneg  9547  elq  9556  qreccl  9576  elpq  9582  ralrp  9607  rexrp  9608  rpnegap  9618  ltxr  9707  xrnemnf  9709  xrltso  9728  icc0r  9858  divelunit  9934  fzprval  10013  fztpval  10014  elfz1b  10021  fz01or  10042  4fvwrd4  10071  fzolb  10084  fzolb2  10085  elfzo3  10094  fzouzsplit  10110  elfzo0z  10115  fzo0m  10122  fzind2  10170  ioo0  10191  ico0  10193  ioc0  10194  uzennn  10367  seq3f1olemp  10433  caucvgre  10919  cvg1nlemcau  10922  resqrexlemex  10963  climeu  11233  fsum2dlemstep  11371  expcnv  11441  prodsnf  11529  fprod2dlemstep  11559  divides  11725  m1exp1  11834  divalgb  11858  bezoutlemnewy  11925  bezoutlemmain  11927  bezoutlemex  11930  dfgcd2  11943  nnwosdc  11968  lcmgcdlem  12005  isprm2  12045  isprm3  12046  isprm4  12047  isprm5  12070  sqrt2irr  12090  oddpwdc  12102  pythagtriplem19  12210  pythagtrip  12211  pceu  12223  dvdsprmpweqnn  12263  4sqlem2  12315  ennnfoneleminc  12340  ennnfonelemex  12343  ennnfonelemr  12352  ctiunct  12369  infpn2  12385  istps  12630  istps2  12631  isbasis2g  12643  tgval2  12651  txuni2  12856  tx1cn  12869  tx2cn  12870  uptx  12874  txdis1cn  12878  blres  13034  xmeterval  13035  xmeter  13036  isxms2  13052  isms2  13054  metrest  13106  qtopbasss  13121  dedekindicclemicc  13210  limcdifap  13231  pilem1  13300  sincosq1lem  13346  2sqlem1  13550  decidr  13637  bdcuni  13718  bdcriota  13725  bdinex1  13741  bj-zfpair2  13752  bj-axun2  13757  bj-ssom  13778  ss1oel2o  13833  nninfsellemdc  13850  nninfsellemsuc  13852  nninfsellemqall  13855  trirec0xor  13884  iswomni0  13890