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  453  anbi2ci  456  anbi12i  457  anbi12ci  458  bianassc  467  pm5.3  472  an42  582  xchbinx  677  mt2bi  679  orbi12i  759  or42  767  pm5.53  797  orddi  815  anddi  816  pm2.1dc  832  dcim  836  notnotrdc  838  dcnnOLD  844  rbaib  916  rbaibr  917  pm4.43  944  orbididc  948  pm5.75  957  3orass  976  3anass  977  3ancomb  981  3anan32  984  3anan12  985  anandi3  986  anandi3r  987  xordc  1387  falbitru  1412  19.26-2  1475  19.26-3an  1476  alrot3  1478  albiim  1480  2albiim  1481  19.27h  1553  19.27  1554  19.28h  1555  19.28  1556  nfalt  1571  aaanh  1579  aaan  1580  alinexa  1596  19.21-2  1660  nf2  1661  19.44  1675  19.45  1676  exrot3  1683  exrot4  1684  eeor  1688  sbcof2  1803  sbid2h  1842  19.23vv  1877  sbnv  1881  sblimv  1887  pm11.53  1888  19.41vv  1896  19.41vvv  1897  19.41vvvv  1898  exdistrv  1903  19.42vv  1904  19.42vvv  1905  19.42vvvv  1906  4exdistr  1909  cbvex4v  1923  eean  1924  sbn  1945  sbim  1946  sbor  1947  sban  1948  sbrim  1949  sblim  1950  sbbi  1952  sblbis  1953  sbrbis  1954  sbrbif  1955  sbco2d  1959  sbco2vd  1960  sbnf2  1974  2sb5  1976  2sb6  1977  sbcom2v  1978  sbcom2v2  1979  sbcom2  1980  sb6a  1981  2sb5rf  1982  2sb6rf  1983  sbalyz  1992  sbal  1993  sbal1yz  1994  sbex  1997  sbalv  1998  sbco4lem  1999  exsb  2001  2exsb  2002  eujust  2021  euf  2024  cbveu  2043  mor  2061  eu2  2063  mo4f  2079  eu4  2081  2exeu  2111  2eu4  2112  exists1  2115  abid  2158  eleq12i  2238  abeq2  2279  abeq2i  2281  clabel  2297  abid2f  2338  sbabel  2339  neeq12i  2357  neanior  2427  ralnex  2458  dfrex2dc  2461  ralinexa  2497  nfraldya  2505  nfrexdya  2506  r3al  2514  r19.26-2  2599  ralbiim  2604  ralnex2  2609  r19.43  2628  ralcomf  2631  rexcomf  2632  rexrot4  2636  reean  2638  3reeanv  2640  rabbi  2647  cbvralf  2689  cbvrexf  2690  cbvreu  2694  cbvral2vw  2707  cbvrex2vw  2708  cbvral2v  2709  cbvrex2v  2710  cbvral3v  2711  cbvralsv  2712  cbvrexsv  2713  sbralie  2714  rabeq2i  2727  issetf  2737  2gencl  2763  3gencl  2764  ceqsex2  2770  ceqsex3v  2772  ceqsex6v  2774  ceqsex8v  2775  gencbvex  2776  gencbval  2778  spc2gv  2821  eqvincf  2855  ceqsrex2v  2862  clel5  2867  elrab2  2889  ralab  2890  ralrab  2891  rexab  2892  rexrab  2893  ralab2  2894  rexab2  2896  eueq3dc  2904  morex  2914  euind  2917  reu2  2918  reu6  2919  rmo4  2923  reu4  2924  reu7  2925  rmo3f  2927  rmo4f  2928  rmoim  2931  2reuswapdc  2934  reuind  2935  2rmorex  2936  sbcco  2976  sbccomlem  3029  sbccom  3030  ra5  3043  rmo3  3046  csbco  3059  csbcow  3060  sbnfc2  3109  csbabg  3110  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  dfss  3135  dfss2f  3138  ss2ab  3215  dfdif3  3237  difeqri  3247  ddifstab  3259  raldifb  3267  uneqri  3269  ssequn2  3300  unss  3301  rexun  3307  ralunb  3308  elin2  3315  ineqri  3320  dfss1  3331  dfss5  3332  dfss4st  3360  ssddif  3361  difin  3364  indif  3370  difundi  3379  indifdir  3383  symdifxor  3393  inrab2  3400  rabun2  3406  reuun2  3410  0el  3437  rabeq0  3444  abeq0  3445  disjr  3464  disj1  3465  undif4  3477  uneqdifeqim  3500  r19.2m  3501  r19.3rm  3503  r19.9rmv  3506  raaan  3521  pwss  3582  dfpr2  3602  rexdifpr  3611  ralsnsg  3620  ralsns  3621  eltpg  3628  eldiftp  3629  ralprg  3634  rexprg  3635  raltpg  3636  rextpg  3637  snprc  3648  rabrsndc  3651  euabsn2  3652  eusn  3657  eldifsn  3710  ssdifsn  3711  rexdifsn  3715  eqsnm  3742  tpss  3745  snsssn  3748  prel12  3758  preqsn  3762  oprcl  3789  pwtpss  3793  eluniab  3808  elunirab  3809  unipr  3810  dfnfc2  3814  uniun  3815  uniin  3816  uni0b  3821  unissb  3826  elintab  3842  elintrab  3843  ssintab  3848  ssintrab  3854  intun  3862  intpr  3863  elrint  3871  iuncom4  3880  iuneq2  3889  dfiun2g  3905  ssiinf  3922  iundif2ss  3938  elriin  3943  iunxiun  3954  pwssb  3958  elpwpw  3959  iunpwss  3964  dfdisj2  3968  disjiun  3984  cbvopab1  4062  dftr5  4090  trint  4102  inex1  4123  inuni  4141  repizf2lem  4147  unidif0  4153  axpweq  4157  bnd2  4159  exmid01  4184  zfpair2  4195  exss  4212  elop  4216  opm  4219  otth  4227  copsex4g  4232  opeqsn  4237  opelopabsbALT  4244  brabga  4249  opelopabaf  4258  iunopab  4266  pwunss  4268  pocl  4288  frirrg  4335  elsuci  4388  elsucg  4389  sucel  4395  unisucg  4399  uniuni  4436  reusv3  4445  iunpw  4465  setindel  4522  elirr  4525  en2lp  4538  ordpwsucss  4551  zfregfr  4558  tfi  4566  peano2  4579  peano5  4582  elxp  4628  opelxp  4641  brxp  4642  rabxp  4648  opthprc  4662  brab2a  4664  opeliunxp  4666  xpundi  4667  xpundir  4668  elvvv  4674  brinxp  4679  brab2ga  4686  0xp  4691  ssrel2  4701  eqrelrel  4712  reliun  4732  reluni  4734  raliunxp  4752  rexiunxp  4753  ralxpf  4757  rexxpf  4758  iunxpf  4759  relop  4761  elco  4777  elcnv  4788  elcnv2  4789  dmin  4819  dmuni  4821  dmopab  4822  dmi  4826  dmmrnm  4830  rnopab  4858  elrnmpt1  4862  rncoeq  4884  resiexg  4936  dfima2  4955  dfima3  4956  elima2  4959  elima3  4960  imai  4967  elimasn  4978  epini  4982  dfse2  4984  cotr  4992  issref  4993  intasym  4995  asymref  4996  cnvopab  5012  cnvi  5015  cnvdif  5017  imainss  5026  rnxpid  5045  dfrel2  5061  dfrel3  5068  dmsnm  5076  rnsnm  5077  relsn2m  5081  dmsnopg  5082  cnvcnvsn  5087  elxp4  5098  elxp5  5099  cnvresima  5100  mptpreima  5104  dfco2  5110  coundi  5112  coundir  5113  imaco  5116  coiun  5120  coi1  5126  relssdmrn  5131  relrelss  5137  unixpm  5146  ressn  5151  cnviinm  5152  cnvpom  5153  cnvsom  5154  cbviota  5165  iotass  5177  eliota  5186  dffun2  5208  dffun4  5209  dffun7  5225  dffun8  5226  dffun9  5227  funopab  5233  funun  5242  funcnvsn  5243  fntpg  5254  funcnv2  5258  funcnv  5259  fun2cnv  5262  fncnv  5264  fun11  5265  fununi  5266  imadiflem  5277  imadif  5278  imainlem  5279  funimaexglem  5281  fnunsn  5305  fnres  5314  fnopabg  5321  mptfng  5323  mptun  5329  fun  5370  fcnvres  5381  dff12  5402  f1cnvcnv  5414  funforn  5427  dff1o2  5447  dff1o5  5451  f1orn  5452  resdif  5464  ffoss  5474  f11o  5475  f1o00  5477  fo00  5478  elfv  5494  fv3  5519  nfvres  5529  eqfnfv3  5595  fneqeql  5604  unpreima  5621  respreima  5624  dffo3  5643  dffo5  5645  f1ompt  5647  ffnfvf  5655  fmptco  5662  ftpg  5680  fnressn  5682  idref  5736  abrexco  5738  dff13  5747  dff13f  5749  fliftel  5772  isoini  5797  eusvobj2  5839  acexmidlema  5844  acexmidlemb  5845  acexmidlemph  5846  acexmidlem2  5850  oprabid  5885  brabvv  5899  dfoprab2  5900  eqoprab2b  5911  dmoprab  5934  rnoprab  5936  eloprabga  5940  mpomptx  5944  resoprab  5949  ffnov  5957  elrnmpo  5966  ralrnmpo  5967  rexrnmpo  5968  ovid  5969  ovi3  5989  ov6g  5990  foov  5999  opabex3d  6100  opabex3  6101  abexssex  6104  oprabex3  6108  oprabrexex2  6109  fmpo  6180  xporderlem  6210  f1od2  6214  mpoxopovel  6220  brtpos2  6230  dmtpos  6235  tpostpos  6243  tpossym  6255  tposoprab  6259  dfsmo2  6266  tfrlem7  6296  tfrlem9  6298  tfr1onlemaccex  6327  tfrcllemaccex  6340  tfrcldm  6342  frecabex  6377  el1o  6416  dif1o  6417  dfer2  6514  brdifun  6540  eqerlem  6544  qsid  6578  iinerm  6585  riinerm  6586  erinxp  6587  brecop  6603  eroveu  6604  erovlem  6605  ecopovsym  6609  mapval2  6656  mapsn  6668  elixp  6683  ixpeq2  6690  ixpin  6701  ixpiinm  6702  mptelixpg  6712  ixpsnf1o  6714  domen  6729  isfi  6739  en1  6777  xpsnen  6799  xpcomco  6804  xpassen  6808  ssenen  6829  nneneq  6835  snnen2oprc  6838  ac6sfi  6876  exmidpw  6886  exmidpweq  6887  pw1dc1  6891  eldju  7045  djur  7046  eldju2ndl  7049  eldju2ndr  7050  finomni  7116  nninfwlporlemd  7148  nninfwlpoimlemg  7151  acfun  7184  pw1nel3  7208  sucpw1nel3  7210  ccfunen  7226  elni  7270  ltexpi  7299  enq0enq  7393  enq0ref  7395  enq0tr  7396  prarloclem3  7459  ltdfpr  7468  genpdflem  7469  genpassl  7486  genpassu  7487  nqprrnd  7505  nqprl  7513  nqpru  7514  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemdisj  7568  ltexprlemloc  7569  recexprlemdisj  7592  caucvgprprlemell  7647  caucvgprprlemelu  7648  suplocexprlemml  7678  suplocsrlemb  7768  opelcn  7788  elreal  7790  elreal2  7792  peano1nnnn  7814  axicn  7825  axaddf  7830  axmulf  7831  axprecex  7842  axpre-ltirr  7844  axpre-mulgt0  7849  axcaucvglemres  7861  axpre-suploc  7864  xrlenlt  7984  ltxrlt  7985  inelr  8503  reapcotr  8517  1nn  8889  elnnne0  9149  un0addcl  9168  un0mulcl  9169  elnnz  9222  elznn0nn  9226  elznn0  9227  elznn  9228  elz2  9283  zapne  9286  3halfnz  9309  prime  9311  raluz2  9538  rexuz2  9540  supinfneg  9554  infsupneg  9555  eluz2b2  9562  eluz2b3  9563  ublbneg  9572  elq  9581  qreccl  9601  elpq  9607  ralrp  9632  rexrp  9633  rpnegap  9643  ltxr  9732  xrnemnf  9734  xrltso  9753  icc0r  9883  divelunit  9959  fzprval  10038  fztpval  10039  elfz1b  10046  fz01or  10067  4fvwrd4  10096  fzolb  10109  fzolb2  10110  elfzo3  10119  fzouzsplit  10135  elfzo0z  10140  fzo0m  10147  fzind2  10195  ioo0  10216  ico0  10218  ioc0  10219  uzennn  10392  seq3f1olemp  10458  caucvgre  10945  cvg1nlemcau  10948  resqrexlemex  10989  climeu  11259  fsum2dlemstep  11397  expcnv  11467  prodsnf  11555  fprod2dlemstep  11585  divides  11751  m1exp1  11860  divalgb  11884  bezoutlemnewy  11951  bezoutlemmain  11953  bezoutlemex  11956  dfgcd2  11969  nnwosdc  11994  lcmgcdlem  12031  isprm2  12071  isprm3  12072  isprm4  12073  isprm5  12096  sqrt2irr  12116  oddpwdc  12128  pythagtriplem19  12236  pythagtrip  12237  pceu  12249  dvdsprmpweqnn  12289  4sqlem2  12341  ennnfoneleminc  12366  ennnfonelemex  12369  ennnfonelemr  12378  ctiunct  12395  infpn2  12411  ismnd  12655  dfgrp2e  12733  istps  12824  istps2  12825  isbasis2g  12837  tgval2  12845  txuni2  13050  tx1cn  13063  tx2cn  13064  uptx  13068  txdis1cn  13072  blres  13228  xmeterval  13229  xmeter  13230  isxms2  13246  isms2  13248  metrest  13300  qtopbasss  13315  dedekindicclemicc  13404  limcdifap  13425  pilem1  13494  sincosq1lem  13540  2sqlem1  13744  decidr  13831  bdcuni  13911  bdcriota  13918  bdinex1  13934  bj-zfpair2  13945  bj-axun2  13950  bj-ssom  13971  ss1oel2o  14026  nninfsellemdc  14043  nninfsellemsuc  14045  nninfsellemqall  14048  trirec0xor  14077  iswomni0  14083