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-1 5  ax-2 6  ax-mp 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  385  biadan2  447  anbi2ci  450  anbi12i  451  anbi12ci  452  pm5.3  462  an42  557  xchbinx  648  mt2bi  650  orbi12i  722  or42  730  pm5.53  757  orddi  775  anddi  776  pm2.1dc  789  notnotrdc  795  dcim  828  testbitestn  867  rbaib  874  rbaibr  875  pm4.43  901  orbididc  905  pm5.75  914  3orass  933  3anass  934  3ancomb  938  3anan32  941  3anan12  942  anandi3  943  anandi3r  944  xordc  1338  falbitru  1363  19.26-2  1426  19.26-3an  1427  alrot3  1429  albiim  1431  2albiim  1432  19.27h  1507  19.27  1508  19.28h  1509  19.28  1510  nfalt  1525  aaanh  1533  aaan  1534  alinexa  1550  19.21-2  1613  nf2  1614  19.44  1628  19.45  1629  exrot3  1636  exrot4  1637  eeor  1641  sbcof2  1749  sbid2h  1788  19.23vv  1823  sbnv  1827  sblimv  1833  pm11.53  1834  19.41vv  1842  19.41vvv  1843  19.41vvvv  1844  exdistrv  1847  19.42vv  1848  19.42vvv  1849  19.42vvvv  1850  4exdistr  1853  cbvex4v  1865  eean  1866  sbn  1886  sbim  1887  sbor  1888  sban  1889  sbrim  1890  sblim  1891  sbbi  1893  sblbis  1894  sbrbis  1895  sbrbif  1896  sbco2d  1900  sbco2vd  1901  sbnf2  1917  2sb5  1919  2sb6  1920  sbcom2v  1921  sbcom2v2  1922  sbcom2  1923  sb6a  1924  2sb5rf  1925  2sb6rf  1926  sbalyz  1935  sbal  1936  sbal1yz  1937  sbex  1940  sbalv  1941  sbco4lem  1942  exsb  1944  2exsb  1945  eujust  1962  euf  1965  cbveu  1984  mor  2002  eu2  2004  mo4f  2020  eu4  2022  2exeu  2052  2eu4  2053  exists1  2056  abid  2088  eleq12i  2167  abeq2  2208  abeq2i  2210  clabel  2225  abid2f  2265  sbabel  2266  neeq12i  2284  neanior  2354  ralnex  2385  dfrex2dc  2387  ralinexa  2421  nfraldya  2428  nfrexdya  2429  r3al  2436  r19.26-2  2520  ralbiim  2525  r19.43  2547  ralcomf  2550  rexcomf  2551  rexrot4  2555  reean  2557  3reeanv  2559  rabbi  2566  cbvralf  2606  cbvrexf  2607  cbvreu  2610  cbvral2v  2620  cbvrex2v  2621  cbvral3v  2622  cbvralsv  2623  cbvrexsv  2624  sbralie  2625  rabeq2i  2638  issetf  2648  2gencl  2674  3gencl  2675  ceqsex2  2681  ceqsex3v  2683  ceqsex6v  2685  ceqsex8v  2686  gencbvex  2687  gencbval  2689  spc2gv  2731  eqvincf  2764  ceqsrex2v  2771  elrab2  2796  ralab  2797  ralrab  2798  rexab  2799  rexrab  2800  ralab2  2801  rexab2  2803  eueq3dc  2811  morex  2821  euind  2824  reu2  2825  reu6  2826  rmo4  2830  reu4  2831  reu7  2832  rmo3f  2834  rmo4f  2835  rmoim  2838  2reuswapdc  2841  reuind  2842  2rmorex  2843  sbcco  2883  sbccomlem  2935  sbccom  2936  ra5  2949  rmo3  2952  csbco  2964  sbnfc2  3010  csbabg  3011  cbvralcsf  3012  cbvrexcsf  3013  cbvreucsf  3014  dfss  3035  dfss2f  3038  ss2ab  3112  dfdif3  3133  difeqri  3143  ddifstab  3155  raldifb  3163  uneqri  3165  ssequn2  3196  unss  3197  rexun  3203  ralunb  3204  elin2  3211  ineqri  3216  dfss1  3227  dfss5  3228  dfss4st  3256  ssddif  3257  difin  3260  indif  3266  difundi  3275  indifdir  3279  symdifxor  3289  inrab2  3296  rabun2  3302  reuun2  3306  0el  3332  rabeq0  3339  abeq0  3340  disjr  3359  disj1  3360  undif4  3372  uneqdifeqim  3395  r19.2m  3396  r19.3rm  3398  r19.9rmv  3401  raaan  3416  pwss  3473  dfpr2  3493  ralsnsg  3508  ralsns  3509  eltpg  3516  ralprg  3521  rexprg  3522  raltpg  3523  rextpg  3524  snprc  3535  rabrsndc  3538  euabsn2  3539  eusn  3544  eldifsn  3597  ssdifsn  3598  rexdifsn  3602  eqsnm  3629  tpss  3632  snsssn  3635  prel12  3645  preqsn  3649  oprcl  3676  pwtpss  3680  eluniab  3695  elunirab  3696  unipr  3697  dfnfc2  3701  uniun  3702  uniin  3703  uni0b  3708  unissb  3713  elintab  3729  elintrab  3730  ssintab  3735  ssintrab  3741  intun  3749  intpr  3750  elrint  3758  iuncom4  3767  iuneq2  3776  dfiun2g  3792  ssiinf  3809  iundif2ss  3825  elriin  3830  iunxiun  3840  pwssb  3844  elpwpw  3845  iunpwss  3850  dfdisj2  3854  disjiun  3870  cbvopab1  3941  dftr5  3969  trint  3981  inex1  4002  inuni  4020  repizf2lem  4025  unidif0  4031  axpweq  4035  bnd2  4037  exmid01  4061  zfpair2  4070  exss  4087  elop  4091  opm  4094  otth  4102  copsex4g  4107  opeqsn  4112  opelopabsbALT  4119  brabga  4124  opelopabaf  4133  iunopab  4141  pwunss  4143  pocl  4163  frirrg  4210  elsuci  4263  elsucg  4264  sucel  4270  unisucg  4274  uniuni  4310  reusv3  4319  iunpw  4339  setindel  4391  elirr  4394  en2lp  4407  ordpwsucss  4420  zfregfr  4426  tfi  4434  peano2  4447  peano5  4450  elxp  4494  opelxp  4507  brxp  4508  rabxp  4514  opthprc  4528  brab2a  4530  opeliunxp  4532  xpundi  4533  xpundir  4534  elvvv  4540  brinxp  4545  brab2ga  4552  0xp  4557  ssrel2  4567  eqrelrel  4578  reliun  4598  reluni  4600  raliunxp  4618  rexiunxp  4619  ralxpf  4623  rexxpf  4624  iunxpf  4625  relop  4627  elco  4643  elcnv  4654  elcnv2  4655  dmin  4685  dmuni  4687  dmopab  4688  dmi  4692  dmmrnm  4696  rnopab  4724  elrnmpt1  4728  rncoeq  4748  resiexg  4800  dfima2  4819  dfima3  4820  elima2  4823  elima3  4824  imai  4831  elimasn  4842  epini  4846  dfse2  4848  cotr  4856  issref  4857  intasym  4859  asymref  4860  cnvopab  4876  cnvi  4879  cnvdif  4881  imainss  4890  rnxpid  4909  dfrel2  4925  dfrel3  4932  dmsnm  4940  rnsnm  4941  relsn2m  4945  dmsnopg  4946  cnvcnvsn  4951  elxp4  4962  elxp5  4963  cnvresima  4964  mptpreima  4968  dfco2  4974  coundi  4976  coundir  4977  imaco  4980  coiun  4984  coi1  4990  relssdmrn  4995  relrelss  5001  unixpm  5010  ressn  5015  cnviinm  5016  cnvpom  5017  cnvsom  5018  cbviota  5029  iotass  5041  dffun2  5069  dffun4  5070  dffun7  5086  dffun8  5087  dffun9  5088  funopab  5094  funun  5103  funcnvsn  5104  fntpg  5115  funcnv2  5119  funcnv  5120  fun2cnv  5123  fncnv  5125  fun11  5126  fununi  5127  imadiflem  5138  imadif  5139  imainlem  5140  funimaexglem  5142  fnunsn  5166  fnres  5175  fnopabg  5182  mptfng  5184  mptun  5190  fun  5231  fcnvres  5242  dff12  5263  f1cnvcnv  5275  funforn  5288  dff1o2  5306  dff1o5  5310  f1orn  5311  resdif  5323  ffoss  5333  f11o  5334  f1o00  5336  fo00  5337  elfv  5351  fv3  5376  nfvres  5386  eqfnfv3  5452  fneqeql  5460  unpreima  5477  respreima  5480  dffo3  5499  dffo5  5501  f1ompt  5503  ffnfvf  5511  fmptco  5518  ftpg  5536  fnressn  5538  idref  5590  abrexco  5592  dff13  5601  dff13f  5603  fliftel  5626  isoini  5651  eusvobj2  5692  acexmidlema  5697  acexmidlemb  5698  acexmidlemph  5699  acexmidlem2  5703  oprabid  5735  brabvv  5749  dfoprab2  5750  eqoprab2b  5761  dmoprab  5784  rnoprab  5786  eloprabga  5790  mpomptx  5794  resoprab  5799  ffnov  5807  elrnmpo  5816  ralrnmpo  5817  rexrnmpo  5818  ovid  5819  ovi3  5839  ov6g  5840  foov  5849  opabex3d  5950  opabex3  5951  abexssex  5954  oprabex3  5958  oprabrexex2  5959  fmpo  6029  xporderlem  6058  f1od2  6062  mpoxopovel  6068  brtpos2  6078  dmtpos  6083  tpostpos  6091  tpossym  6103  tposoprab  6107  dfsmo2  6114  tfrlem7  6144  tfrlem9  6146  tfr1onlemaccex  6175  tfrcllemaccex  6188  tfrcldm  6190  frecabex  6225  el1o  6264  dif1o  6265  dfer2  6360  brdifun  6386  eqerlem  6390  qsid  6424  iinerm  6431  riinerm  6432  erinxp  6433  brecop  6449  eroveu  6450  erovlem  6451  ecopovsym  6455  mapval2  6502  mapsn  6514  elixp  6529  ixpeq2  6536  ixpin  6547  ixpiinm  6548  mptelixpg  6558  ixpsnf1o  6560  domen  6575  isfi  6585  en1  6623  xpsnen  6644  xpcomco  6649  xpassen  6653  ssenen  6674  nneneq  6680  snnen2oprc  6683  ac6sfi  6721  exmidpw  6731  eldju  6868  djur  6869  eldju2ndl  6872  eldju2ndr  6873  finomni  6924  elni  7017  ltexpi  7046  enq0enq  7140  enq0ref  7142  enq0tr  7143  prarloclem3  7206  ltdfpr  7215  genpdflem  7216  genpassl  7233  genpassu  7234  nqprrnd  7252  nqprl  7260  nqpru  7261  ltexprlemopl  7310  ltexprlemopu  7312  ltexprlemdisj  7315  ltexprlemloc  7316  recexprlemdisj  7339  caucvgprprlemell  7394  caucvgprprlemelu  7395  opelcn  7514  elreal  7516  elreal2  7518  peano1nnnn  7539  axicn  7550  axprecex  7565  axpre-ltirr  7567  axpre-mulgt0  7572  axcaucvglemres  7584  xrlenlt  7701  ltxrlt  7702  inelr  8212  reapcotr  8226  1nn  8589  elnnne0  8843  un0addcl  8862  un0mulcl  8863  elnnz  8916  elznn0nn  8920  elznn0  8921  elznn  8922  elz2  8974  zapne  8977  3halfnz  9000  prime  9002  raluz2  9224  rexuz2  9226  supinfneg  9240  infsupneg  9241  eluz2b2  9247  eluz2b3  9248  ublbneg  9255  elq  9264  qreccl  9284  ralrp  9312  rexrp  9313  rpnegap  9323  ltxr  9403  xrnemnf  9405  xrltso  9423  icc0r  9550  divelunit  9626  fzprval  9703  fztpval  9704  elfz1b  9711  fz01or  9732  4fvwrd4  9758  fzolb  9771  fzolb2  9772  elfzo3  9781  fzouzsplit  9797  elfzo0z  9802  fzo0m  9809  fzind2  9857  ioo0  9878  ico0  9880  ioc0  9881  uzennn  10050  seq3f1olemp  10116  caucvgre  10593  cvg1nlemcau  10596  resqrexlemex  10637  climeu  10904  fsum2dlemstep  11042  expcnv  11112  divides  11290  m1exp1  11393  divalgb  11417  bezoutlemnewy  11477  bezoutlemmain  11479  bezoutlemex  11482  dfgcd2  11495  lcmgcdlem  11551  isprm2  11591  isprm3  11592  isprm4  11593  sqrt2irr  11633  oddpwdc  11644  ennnfoneleminc  11716  ennnfonelemex  11719  ennnfonelemr  11728  istps  11981  istps2  11982  isbasis2g  11994  tgval2  12002  txuni2  12206  tx1cn  12219  tx2cn  12220  uptx  12224  txdis1cn  12228  blres  12362  xmeterval  12363  xmeter  12364  isxms2  12380  isms2  12382  metrest  12434  qtopbasss  12443  limcdifap  12512  decidr  12584  bdcuni  12655  bdcriota  12662  bdinex1  12678  bj-zfpair2  12689  bj-axun2  12694  bj-ssom  12719  ss1oel2o  12774  nninfsellemdc  12790  nninfsellemsuc  12792  nninfsellemqall  12795