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  387  biadan2  451  anbi2ci  454  anbi12i  455  anbi12ci  456  pm5.3  466  an42  576  xchbinx  671  mt2bi  673  orbi12i  753  or42  761  pm5.53  791  orddi  809  anddi  810  pm2.1dc  822  dcim  826  notnotrdc  828  dcnnOLD  834  rbaib  906  rbaibr  907  pm4.43  933  orbididc  937  pm5.75  946  3orass  965  3anass  966  3ancomb  970  3anan32  973  3anan12  974  anandi3  975  anandi3r  976  xordc  1370  falbitru  1395  19.26-2  1458  19.26-3an  1459  alrot3  1461  albiim  1463  2albiim  1464  19.27h  1539  19.27  1540  19.28h  1541  19.28  1542  nfalt  1557  aaanh  1565  aaan  1566  alinexa  1582  19.21-2  1645  nf2  1646  19.44  1660  19.45  1661  exrot3  1668  exrot4  1669  eeor  1673  sbcof2  1782  sbid2h  1821  19.23vv  1856  sbnv  1860  sblimv  1866  pm11.53  1867  19.41vv  1875  19.41vvv  1876  19.41vvvv  1877  exdistrv  1882  19.42vv  1883  19.42vvv  1884  19.42vvvv  1885  4exdistr  1888  cbvex4v  1902  eean  1903  sbn  1925  sbim  1926  sbor  1927  sban  1928  sbrim  1929  sblim  1930  sbbi  1932  sblbis  1933  sbrbis  1934  sbrbif  1935  sbco2d  1939  sbco2vd  1940  sbnf2  1956  2sb5  1958  2sb6  1959  sbcom2v  1960  sbcom2v2  1961  sbcom2  1962  sb6a  1963  2sb5rf  1964  2sb6rf  1965  sbalyz  1974  sbal  1975  sbal1yz  1976  sbex  1979  sbalv  1980  sbco4lem  1981  exsb  1983  2exsb  1984  eujust  2001  euf  2004  cbveu  2023  mor  2041  eu2  2043  mo4f  2059  eu4  2061  2exeu  2091  2eu4  2092  exists1  2095  abid  2127  eleq12i  2207  abeq2  2248  abeq2i  2250  clabel  2266  abid2f  2306  sbabel  2307  neeq12i  2325  neanior  2395  ralnex  2426  dfrex2dc  2428  ralinexa  2462  nfraldya  2469  nfrexdya  2470  r3al  2477  r19.26-2  2561  ralbiim  2566  ralnex2  2571  r19.43  2589  ralcomf  2592  rexcomf  2593  rexrot4  2597  reean  2599  3reeanv  2601  rabbi  2608  cbvralf  2648  cbvrexf  2649  cbvreu  2652  cbvral2v  2665  cbvrex2v  2666  cbvral3v  2667  cbvralsv  2668  cbvrexsv  2669  sbralie  2670  rabeq2i  2683  issetf  2693  2gencl  2719  3gencl  2720  ceqsex2  2726  ceqsex3v  2728  ceqsex6v  2730  ceqsex8v  2731  gencbvex  2732  gencbval  2734  spc2gv  2776  eqvincf  2810  ceqsrex2v  2817  elrab2  2843  ralab  2844  ralrab  2845  rexab  2846  rexrab  2847  ralab2  2848  rexab2  2850  eueq3dc  2858  morex  2868  euind  2871  reu2  2872  reu6  2873  rmo4  2877  reu4  2878  reu7  2879  rmo3f  2881  rmo4f  2882  rmoim  2885  2reuswapdc  2888  reuind  2889  2rmorex  2890  sbcco  2930  sbccomlem  2983  sbccom  2984  ra5  2997  rmo3  3000  csbco  3013  sbnfc2  3060  csbabg  3061  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  dfss  3085  dfss2f  3088  ss2ab  3165  dfdif3  3186  difeqri  3196  ddifstab  3208  raldifb  3216  uneqri  3218  ssequn2  3249  unss  3250  rexun  3256  ralunb  3257  elin2  3264  ineqri  3269  dfss1  3280  dfss5  3281  dfss4st  3309  ssddif  3310  difin  3313  indif  3319  difundi  3328  indifdir  3332  symdifxor  3342  inrab2  3349  rabun2  3355  reuun2  3359  0el  3385  rabeq0  3392  abeq0  3393  disjr  3412  disj1  3413  undif4  3425  uneqdifeqim  3448  r19.2m  3449  r19.3rm  3451  r19.9rmv  3454  raaan  3469  pwss  3526  dfpr2  3546  ralsnsg  3561  ralsns  3562  eltpg  3569  ralprg  3574  rexprg  3575  raltpg  3576  rextpg  3577  snprc  3588  rabrsndc  3591  euabsn2  3592  eusn  3597  eldifsn  3650  ssdifsn  3651  rexdifsn  3655  eqsnm  3682  tpss  3685  snsssn  3688  prel12  3698  preqsn  3702  oprcl  3729  pwtpss  3733  eluniab  3748  elunirab  3749  unipr  3750  dfnfc2  3754  uniun  3755  uniin  3756  uni0b  3761  unissb  3766  elintab  3782  elintrab  3783  ssintab  3788  ssintrab  3794  intun  3802  intpr  3803  elrint  3811  iuncom4  3820  iuneq2  3829  dfiun2g  3845  ssiinf  3862  iundif2ss  3878  elriin  3883  iunxiun  3894  pwssb  3898  elpwpw  3899  iunpwss  3904  dfdisj2  3908  disjiun  3924  cbvopab1  4001  dftr5  4029  trint  4041  inex1  4062  inuni  4080  repizf2lem  4085  unidif0  4091  axpweq  4095  bnd2  4097  exmid01  4121  zfpair2  4132  exss  4149  elop  4153  opm  4156  otth  4164  copsex4g  4169  opeqsn  4174  opelopabsbALT  4181  brabga  4186  opelopabaf  4195  iunopab  4203  pwunss  4205  pocl  4225  frirrg  4272  elsuci  4325  elsucg  4326  sucel  4332  unisucg  4336  uniuni  4372  reusv3  4381  iunpw  4401  setindel  4453  elirr  4456  en2lp  4469  ordpwsucss  4482  zfregfr  4488  tfi  4496  peano2  4509  peano5  4512  elxp  4556  opelxp  4569  brxp  4570  rabxp  4576  opthprc  4590  brab2a  4592  opeliunxp  4594  xpundi  4595  xpundir  4596  elvvv  4602  brinxp  4607  brab2ga  4614  0xp  4619  ssrel2  4629  eqrelrel  4640  reliun  4660  reluni  4662  raliunxp  4680  rexiunxp  4681  ralxpf  4685  rexxpf  4686  iunxpf  4687  relop  4689  elco  4705  elcnv  4716  elcnv2  4717  dmin  4747  dmuni  4749  dmopab  4750  dmi  4754  dmmrnm  4758  rnopab  4786  elrnmpt1  4790  rncoeq  4812  resiexg  4864  dfima2  4883  dfima3  4884  elima2  4887  elima3  4888  imai  4895  elimasn  4906  epini  4910  dfse2  4912  cotr  4920  issref  4921  intasym  4923  asymref  4924  cnvopab  4940  cnvi  4943  cnvdif  4945  imainss  4954  rnxpid  4973  dfrel2  4989  dfrel3  4996  dmsnm  5004  rnsnm  5005  relsn2m  5009  dmsnopg  5010  cnvcnvsn  5015  elxp4  5026  elxp5  5027  cnvresima  5028  mptpreima  5032  dfco2  5038  coundi  5040  coundir  5041  imaco  5044  coiun  5048  coi1  5054  relssdmrn  5059  relrelss  5065  unixpm  5074  ressn  5079  cnviinm  5080  cnvpom  5081  cnvsom  5082  cbviota  5093  iotass  5105  dffun2  5133  dffun4  5134  dffun7  5150  dffun8  5151  dffun9  5152  funopab  5158  funun  5167  funcnvsn  5168  fntpg  5179  funcnv2  5183  funcnv  5184  fun2cnv  5187  fncnv  5189  fun11  5190  fununi  5191  imadiflem  5202  imadif  5203  imainlem  5204  funimaexglem  5206  fnunsn  5230  fnres  5239  fnopabg  5246  mptfng  5248  mptun  5254  fun  5295  fcnvres  5306  dff12  5327  f1cnvcnv  5339  funforn  5352  dff1o2  5372  dff1o5  5376  f1orn  5377  resdif  5389  ffoss  5399  f11o  5400  f1o00  5402  fo00  5403  elfv  5419  fv3  5444  nfvres  5454  eqfnfv3  5520  fneqeql  5528  unpreima  5545  respreima  5548  dffo3  5567  dffo5  5569  f1ompt  5571  ffnfvf  5579  fmptco  5586  ftpg  5604  fnressn  5606  idref  5658  abrexco  5660  dff13  5669  dff13f  5671  fliftel  5694  isoini  5719  eusvobj2  5760  acexmidlema  5765  acexmidlemb  5766  acexmidlemph  5767  acexmidlem2  5771  oprabid  5803  brabvv  5817  dfoprab2  5818  eqoprab2b  5829  dmoprab  5852  rnoprab  5854  eloprabga  5858  mpomptx  5862  resoprab  5867  ffnov  5875  elrnmpo  5884  ralrnmpo  5885  rexrnmpo  5886  ovid  5887  ovi3  5907  ov6g  5908  foov  5917  opabex3d  6019  opabex3  6020  abexssex  6023  oprabex3  6027  oprabrexex2  6028  fmpo  6099  xporderlem  6128  f1od2  6132  mpoxopovel  6138  brtpos2  6148  dmtpos  6153  tpostpos  6161  tpossym  6173  tposoprab  6177  dfsmo2  6184  tfrlem7  6214  tfrlem9  6216  tfr1onlemaccex  6245  tfrcllemaccex  6258  tfrcldm  6260  frecabex  6295  el1o  6334  dif1o  6335  dfer2  6430  brdifun  6456  eqerlem  6460  qsid  6494  iinerm  6501  riinerm  6502  erinxp  6503  brecop  6519  eroveu  6520  erovlem  6521  ecopovsym  6525  mapval2  6572  mapsn  6584  elixp  6599  ixpeq2  6606  ixpin  6617  ixpiinm  6618  mptelixpg  6628  ixpsnf1o  6630  domen  6645  isfi  6655  en1  6693  xpsnen  6715  xpcomco  6720  xpassen  6724  ssenen  6745  nneneq  6751  snnen2oprc  6754  ac6sfi  6792  exmidpw  6802  eldju  6953  djur  6954  eldju2ndl  6957  eldju2ndr  6958  finomni  7012  acfun  7063  ccfunen  7079  elni  7116  ltexpi  7145  enq0enq  7239  enq0ref  7241  enq0tr  7242  prarloclem3  7305  ltdfpr  7314  genpdflem  7315  genpassl  7332  genpassu  7333  nqprrnd  7351  nqprl  7359  nqpru  7360  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemdisj  7414  ltexprlemloc  7415  recexprlemdisj  7438  caucvgprprlemell  7493  caucvgprprlemelu  7494  suplocexprlemml  7524  suplocsrlemb  7614  opelcn  7634  elreal  7636  elreal2  7638  peano1nnnn  7660  axicn  7671  axaddf  7676  axmulf  7677  axprecex  7688  axpre-ltirr  7690  axpre-mulgt0  7695  axcaucvglemres  7707  axpre-suploc  7710  xrlenlt  7829  ltxrlt  7830  inelr  8346  reapcotr  8360  1nn  8731  elnnne0  8991  un0addcl  9010  un0mulcl  9011  elnnz  9064  elznn0nn  9068  elznn0  9069  elznn  9070  elz2  9122  zapne  9125  3halfnz  9148  prime  9150  raluz2  9374  rexuz2  9376  supinfneg  9390  infsupneg  9391  eluz2b2  9397  eluz2b3  9398  ublbneg  9405  elq  9414  qreccl  9434  ralrp  9463  rexrp  9464  rpnegap  9474  ltxr  9562  xrnemnf  9564  xrltso  9582  icc0r  9709  divelunit  9785  fzprval  9862  fztpval  9863  elfz1b  9870  fz01or  9891  4fvwrd4  9917  fzolb  9930  fzolb2  9931  elfzo3  9940  fzouzsplit  9956  elfzo0z  9961  fzo0m  9968  fzind2  10016  ioo0  10037  ico0  10039  ioc0  10040  uzennn  10209  seq3f1olemp  10275  caucvgre  10753  cvg1nlemcau  10756  resqrexlemex  10797  climeu  11065  fsum2dlemstep  11203  expcnv  11273  divides  11495  m1exp1  11598  divalgb  11622  bezoutlemnewy  11684  bezoutlemmain  11686  bezoutlemex  11689  dfgcd2  11702  lcmgcdlem  11758  isprm2  11798  isprm3  11799  isprm4  11800  sqrt2irr  11840  oddpwdc  11852  ennnfoneleminc  11924  ennnfonelemex  11927  ennnfonelemr  11936  ctiunct  11953  istps  12199  istps2  12200  isbasis2g  12212  tgval2  12220  txuni2  12425  tx1cn  12438  tx2cn  12439  uptx  12443  txdis1cn  12447  blres  12603  xmeterval  12604  xmeter  12605  isxms2  12621  isms2  12623  metrest  12675  qtopbasss  12690  dedekindicclemicc  12779  limcdifap  12800  pilem1  12860  sincosq1lem  12906  decidr  13003  bdcuni  13074  bdcriota  13081  bdinex1  13097  bj-zfpair2  13108  bj-axun2  13113  bj-ssom  13134  ss1oel2o  13189  nninfsellemdc  13206  nninfsellemsuc  13208  nninfsellemqall  13211