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  823  dcim  827  notnotrdc  829  dcnnOLD  835  rbaib  907  rbaibr  908  pm4.43  934  orbididc  938  pm5.75  947  3orass  966  3anass  967  3ancomb  971  3anan32  974  3anan12  975  anandi3  976  anandi3r  977  xordc  1371  falbitru  1396  19.26-2  1459  19.26-3an  1460  alrot3  1462  albiim  1464  2albiim  1465  19.27h  1540  19.27  1541  19.28h  1542  19.28  1543  nfalt  1558  aaanh  1566  aaan  1567  alinexa  1583  19.21-2  1646  nf2  1647  19.44  1661  19.45  1662  exrot3  1669  exrot4  1670  eeor  1674  sbcof2  1783  sbid2h  1822  19.23vv  1857  sbnv  1861  sblimv  1867  pm11.53  1868  19.41vv  1876  19.41vvv  1877  19.41vvvv  1878  exdistrv  1883  19.42vv  1884  19.42vvv  1885  19.42vvvv  1886  4exdistr  1889  cbvex4v  1903  eean  1904  sbn  1926  sbim  1927  sbor  1928  sban  1929  sbrim  1930  sblim  1931  sbbi  1933  sblbis  1934  sbrbis  1935  sbrbif  1936  sbco2d  1940  sbco2vd  1941  sbnf2  1957  2sb5  1959  2sb6  1960  sbcom2v  1961  sbcom2v2  1962  sbcom2  1963  sb6a  1964  2sb5rf  1965  2sb6rf  1966  sbalyz  1975  sbal  1976  sbal1yz  1977  sbex  1980  sbalv  1981  sbco4lem  1982  exsb  1984  2exsb  1985  eujust  2002  euf  2005  cbveu  2024  mor  2042  eu2  2044  mo4f  2060  eu4  2062  2exeu  2092  2eu4  2093  exists1  2096  abid  2128  eleq12i  2208  abeq2  2249  abeq2i  2251  clabel  2267  abid2f  2307  sbabel  2308  neeq12i  2326  neanior  2396  ralnex  2427  dfrex2dc  2429  ralinexa  2465  nfraldya  2472  nfrexdya  2473  r3al  2480  r19.26-2  2564  ralbiim  2569  ralnex2  2574  r19.43  2592  ralcomf  2595  rexcomf  2596  rexrot4  2600  reean  2602  3reeanv  2604  rabbi  2611  cbvralf  2651  cbvrexf  2652  cbvreu  2655  cbvral2v  2668  cbvrex2v  2669  cbvral3v  2670  cbvralsv  2671  cbvrexsv  2672  sbralie  2673  rabeq2i  2686  issetf  2696  2gencl  2722  3gencl  2723  ceqsex2  2729  ceqsex3v  2731  ceqsex6v  2733  ceqsex8v  2734  gencbvex  2735  gencbval  2737  spc2gv  2780  eqvincf  2814  ceqsrex2v  2821  elrab2  2847  ralab  2848  ralrab  2849  rexab  2850  rexrab  2851  ralab2  2852  rexab2  2854  eueq3dc  2862  morex  2872  euind  2875  reu2  2876  reu6  2877  rmo4  2881  reu4  2882  reu7  2883  rmo3f  2885  rmo4f  2886  rmoim  2889  2reuswapdc  2892  reuind  2893  2rmorex  2894  sbcco  2934  sbccomlem  2987  sbccom  2988  ra5  3001  rmo3  3004  csbco  3017  sbnfc2  3065  csbabg  3066  cbvralcsf  3067  cbvrexcsf  3068  cbvreucsf  3069  dfss  3090  dfss2f  3093  ss2ab  3170  dfdif3  3191  difeqri  3201  ddifstab  3213  raldifb  3221  uneqri  3223  ssequn2  3254  unss  3255  rexun  3261  ralunb  3262  elin2  3269  ineqri  3274  dfss1  3285  dfss5  3286  dfss4st  3314  ssddif  3315  difin  3318  indif  3324  difundi  3333  indifdir  3337  symdifxor  3347  inrab2  3354  rabun2  3360  reuun2  3364  0el  3390  rabeq0  3397  abeq0  3398  disjr  3417  disj1  3418  undif4  3430  uneqdifeqim  3453  r19.2m  3454  r19.3rm  3456  r19.9rmv  3459  raaan  3474  pwss  3531  dfpr2  3551  rexdifpr  3560  ralsnsg  3568  ralsns  3569  eltpg  3576  eldiftp  3577  ralprg  3582  rexprg  3583  raltpg  3584  rextpg  3585  snprc  3596  rabrsndc  3599  euabsn2  3600  eusn  3605  eldifsn  3658  ssdifsn  3659  rexdifsn  3663  eqsnm  3690  tpss  3693  snsssn  3696  prel12  3706  preqsn  3710  oprcl  3737  pwtpss  3741  eluniab  3756  elunirab  3757  unipr  3758  dfnfc2  3762  uniun  3763  uniin  3764  uni0b  3769  unissb  3774  elintab  3790  elintrab  3791  ssintab  3796  ssintrab  3802  intun  3810  intpr  3811  elrint  3819  iuncom4  3828  iuneq2  3837  dfiun2g  3853  ssiinf  3870  iundif2ss  3886  elriin  3891  iunxiun  3902  pwssb  3906  elpwpw  3907  iunpwss  3912  dfdisj2  3916  disjiun  3932  cbvopab1  4009  dftr5  4037  trint  4049  inex1  4070  inuni  4088  repizf2lem  4093  unidif0  4099  axpweq  4103  bnd2  4105  exmid01  4129  zfpair2  4140  exss  4157  elop  4161  opm  4164  otth  4172  copsex4g  4177  opeqsn  4182  opelopabsbALT  4189  brabga  4194  opelopabaf  4203  iunopab  4211  pwunss  4213  pocl  4233  frirrg  4280  elsuci  4333  elsucg  4334  sucel  4340  unisucg  4344  uniuni  4380  reusv3  4389  iunpw  4409  setindel  4461  elirr  4464  en2lp  4477  ordpwsucss  4490  zfregfr  4496  tfi  4504  peano2  4517  peano5  4520  elxp  4564  opelxp  4577  brxp  4578  rabxp  4584  opthprc  4598  brab2a  4600  opeliunxp  4602  xpundi  4603  xpundir  4604  elvvv  4610  brinxp  4615  brab2ga  4622  0xp  4627  ssrel2  4637  eqrelrel  4648  reliun  4668  reluni  4670  raliunxp  4688  rexiunxp  4689  ralxpf  4693  rexxpf  4694  iunxpf  4695  relop  4697  elco  4713  elcnv  4724  elcnv2  4725  dmin  4755  dmuni  4757  dmopab  4758  dmi  4762  dmmrnm  4766  rnopab  4794  elrnmpt1  4798  rncoeq  4820  resiexg  4872  dfima2  4891  dfima3  4892  elima2  4895  elima3  4896  imai  4903  elimasn  4914  epini  4918  dfse2  4920  cotr  4928  issref  4929  intasym  4931  asymref  4932  cnvopab  4948  cnvi  4951  cnvdif  4953  imainss  4962  rnxpid  4981  dfrel2  4997  dfrel3  5004  dmsnm  5012  rnsnm  5013  relsn2m  5017  dmsnopg  5018  cnvcnvsn  5023  elxp4  5034  elxp5  5035  cnvresima  5036  mptpreima  5040  dfco2  5046  coundi  5048  coundir  5049  imaco  5052  coiun  5056  coi1  5062  relssdmrn  5067  relrelss  5073  unixpm  5082  ressn  5087  cnviinm  5088  cnvpom  5089  cnvsom  5090  cbviota  5101  iotass  5113  dffun2  5141  dffun4  5142  dffun7  5158  dffun8  5159  dffun9  5160  funopab  5166  funun  5175  funcnvsn  5176  fntpg  5187  funcnv2  5191  funcnv  5192  fun2cnv  5195  fncnv  5197  fun11  5198  fununi  5199  imadiflem  5210  imadif  5211  imainlem  5212  funimaexglem  5214  fnunsn  5238  fnres  5247  fnopabg  5254  mptfng  5256  mptun  5262  fun  5303  fcnvres  5314  dff12  5335  f1cnvcnv  5347  funforn  5360  dff1o2  5380  dff1o5  5384  f1orn  5385  resdif  5397  ffoss  5407  f11o  5408  f1o00  5410  fo00  5411  elfv  5427  fv3  5452  nfvres  5462  eqfnfv3  5528  fneqeql  5536  unpreima  5553  respreima  5556  dffo3  5575  dffo5  5577  f1ompt  5579  ffnfvf  5587  fmptco  5594  ftpg  5612  fnressn  5614  idref  5666  abrexco  5668  dff13  5677  dff13f  5679  fliftel  5702  isoini  5727  eusvobj2  5768  acexmidlema  5773  acexmidlemb  5774  acexmidlemph  5775  acexmidlem2  5779  oprabid  5811  brabvv  5825  dfoprab2  5826  eqoprab2b  5837  dmoprab  5860  rnoprab  5862  eloprabga  5866  mpomptx  5870  resoprab  5875  ffnov  5883  elrnmpo  5892  ralrnmpo  5893  rexrnmpo  5894  ovid  5895  ovi3  5915  ov6g  5916  foov  5925  opabex3d  6027  opabex3  6028  abexssex  6031  oprabex3  6035  oprabrexex2  6036  fmpo  6107  xporderlem  6136  f1od2  6140  mpoxopovel  6146  brtpos2  6156  dmtpos  6161  tpostpos  6169  tpossym  6181  tposoprab  6185  dfsmo2  6192  tfrlem7  6222  tfrlem9  6224  tfr1onlemaccex  6253  tfrcllemaccex  6266  tfrcldm  6268  frecabex  6303  el1o  6342  dif1o  6343  dfer2  6438  brdifun  6464  eqerlem  6468  qsid  6502  iinerm  6509  riinerm  6510  erinxp  6511  brecop  6527  eroveu  6528  erovlem  6529  ecopovsym  6533  mapval2  6580  mapsn  6592  elixp  6607  ixpeq2  6614  ixpin  6625  ixpiinm  6626  mptelixpg  6636  ixpsnf1o  6638  domen  6653  isfi  6663  en1  6701  xpsnen  6723  xpcomco  6728  xpassen  6732  ssenen  6753  nneneq  6759  snnen2oprc  6762  ac6sfi  6800  exmidpw  6810  eldju  6961  djur  6962  eldju2ndl  6965  eldju2ndr  6966  finomni  7020  acfun  7080  ccfunen  7096  elni  7140  ltexpi  7169  enq0enq  7263  enq0ref  7265  enq0tr  7266  prarloclem3  7329  ltdfpr  7338  genpdflem  7339  genpassl  7356  genpassu  7357  nqprrnd  7375  nqprl  7383  nqpru  7384  ltexprlemopl  7433  ltexprlemopu  7435  ltexprlemdisj  7438  ltexprlemloc  7439  recexprlemdisj  7462  caucvgprprlemell  7517  caucvgprprlemelu  7518  suplocexprlemml  7548  suplocsrlemb  7638  opelcn  7658  elreal  7660  elreal2  7662  peano1nnnn  7684  axicn  7695  axaddf  7700  axmulf  7701  axprecex  7712  axpre-ltirr  7714  axpre-mulgt0  7719  axcaucvglemres  7731  axpre-suploc  7734  xrlenlt  7853  ltxrlt  7854  inelr  8370  reapcotr  8384  1nn  8755  elnnne0  9015  un0addcl  9034  un0mulcl  9035  elnnz  9088  elznn0nn  9092  elznn0  9093  elznn  9094  elz2  9146  zapne  9149  3halfnz  9172  prime  9174  raluz2  9401  rexuz2  9403  supinfneg  9417  infsupneg  9418  eluz2b2  9424  eluz2b3  9425  ublbneg  9432  elq  9441  qreccl  9461  elpq  9467  ralrp  9492  rexrp  9493  rpnegap  9503  ltxr  9592  xrnemnf  9594  xrltso  9612  icc0r  9739  divelunit  9815  fzprval  9893  fztpval  9894  elfz1b  9901  fz01or  9922  4fvwrd4  9948  fzolb  9961  fzolb2  9962  elfzo3  9971  fzouzsplit  9987  elfzo0z  9992  fzo0m  9999  fzind2  10047  ioo0  10068  ico0  10070  ioc0  10071  uzennn  10240  seq3f1olemp  10306  caucvgre  10785  cvg1nlemcau  10788  resqrexlemex  10829  climeu  11097  fsum2dlemstep  11235  expcnv  11305  divides  11531  m1exp1  11634  divalgb  11658  bezoutlemnewy  11720  bezoutlemmain  11722  bezoutlemex  11725  dfgcd2  11738  lcmgcdlem  11794  isprm2  11834  isprm3  11835  isprm4  11836  sqrt2irr  11876  oddpwdc  11888  ennnfoneleminc  11960  ennnfonelemex  11963  ennnfonelemr  11972  ctiunct  11989  istps  12238  istps2  12239  isbasis2g  12251  tgval2  12259  txuni2  12464  tx1cn  12477  tx2cn  12478  uptx  12482  txdis1cn  12486  blres  12642  xmeterval  12643  xmeter  12644  isxms2  12660  isms2  12662  metrest  12714  qtopbasss  12729  dedekindicclemicc  12818  limcdifap  12839  pilem1  12908  sincosq1lem  12954  decidr  13174  bdcuni  13245  bdcriota  13252  bdinex1  13268  bj-zfpair2  13279  bj-axun2  13284  bj-ssom  13305  ss1oel2o  13360  nninfsellemdc  13381  nninfsellemsuc  13383  nninfsellemqall  13386  trirec0xor  13413