Theorem bitri 184

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 120	. . 3 |- ( ph -> ps )
3		bitri.2	. . 3 |- ( ps <-> ch )
4	2, 3	sylib 122	. 2 |- ( ph -> ch )
5	3	biimpri 133	. . 3 |- ( ch -> ps )
6	5, 1	sylibr 134	. 2 |- ( ch -> ph )
7	4, 6	impbii 126	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bitr2i  185  bitr3i  186  bitr4i  187  bitrd  188  3bitri  206  3bitr2i  208  3bitr3i  210  3bitr4i  212  bibi12i  229  imbi12i  239  pm4.71r  390  biadan2  456  anbi2ci  459  anbi12i  460  anbi12ci  461  bianassc  470  pm5.3  475  an42  587  xchbinx  683  mt2bi  685  orbi12i  765  or42  773  pm5.53  803  orddi  821  anddi  822  pm2.1dc  838  dcim  842  notnotrdc  844  dcnnOLD  850  rbaib  922  rbaibr  923  pm4.43  951  orbididc  955  pm5.75  964  3orass  983  3anass  984  3ancomb  988  3anan32  991  3anan12  992  anandi3  993  anandi3r  994  xordc  1403  falbitru  1428  19.26-2  1493  19.26-3an  1494  alrot3  1496  albiim  1498  2albiim  1499  19.27h  1571  19.27  1572  19.28h  1573  19.28  1574  nfalt  1589  aaanh  1597  aaan  1598  alinexa  1614  19.21-2  1678  nf2  1679  19.44  1693  19.45  1694  exrot3  1701  exrot4  1702  eeor  1706  sbcof2  1821  sbid2h  1860  19.23vv  1895  sbnv  1900  sblimv  1906  pm11.53  1907  19.41vv  1915  19.41vvv  1916  19.41vvvv  1917  exdistrv  1922  19.42vv  1923  19.42vvv  1924  19.42vvvv  1925  4exdistr  1928  cbvex4v  1942  eean  1943  sbn  1964  sbim  1965  sbor  1966  sban  1967  sbrim  1968  sblim  1969  sbbi  1971  sblbis  1972  sbrbis  1973  sbrbif  1974  sbco2d  1978  sbco2vd  1979  sbnf2  1993  2sb5  1995  2sb6  1996  sbcom2v  1997  sbcom2v2  1998  sbcom2  1999  sb6a  2000  2sb5rf  2001  2sb6rf  2002  sbalyz  2011  sbal  2012  sbal1yz  2013  sbex  2016  sbalv  2017  sbco4lem  2018  exsb  2020  2exsb  2021  eujust  2040  euf  2043  cbveu  2062  mor  2080  eu2  2082  mo4f  2098  eu4  2100  2exeu  2130  2eu4  2131  exists1  2134  abid  2177  eleq12i  2257  abeq2  2298  abeq2i  2300  clabel  2316  abid2f  2358  sbabel  2359  neeq12i  2377  neanior  2447  ralnex  2478  dfrex2dc  2481  ralinexa  2517  nfraldya  2525  nfrexdya  2526  r3al  2534  r19.26-2  2619  ralbiim  2624  ralnex2  2629  r19.43  2648  ralcomf  2651  rexcomf  2652  ralrot3  2655  rexrot4  2657  reean  2659  3reeanv  2661  rabbi  2668  cbvralf  2710  cbvrexf  2711  cbvreu  2716  cbvral2vw  2729  cbvrex2vw  2730  cbvral2v  2731  cbvrex2v  2732  cbvral3v  2733  cbvralsv  2734  cbvrexsv  2735  sbralie  2736  rabeq2i  2749  issetf  2759  2gencl  2785  3gencl  2786  ceqsex2  2792  ceqsex3v  2794  ceqsex6v  2796  ceqsex8v  2797  gencbvex  2798  gencbval  2800  spc2gv  2843  eqvincf  2877  ceqsrex2v  2884  clel5  2889  elrab2  2911  ralab  2912  ralrab  2913  rexab  2914  rexrab  2915  ralab2  2916  rexab2  2918  eueq3dc  2926  morex  2936  euind  2939  reu2  2940  reu6  2941  rmo4  2945  reu4  2946  reu7  2947  rmo3f  2949  rmo4f  2950  rmoim  2953  2reuswapdc  2956  reuind  2957  2rmorex  2958  sbcco  2999  sbccomlem  3052  sbccom  3053  ra5  3066  rmo3  3069  csbco  3082  csbcow  3083  sbnfc2  3132  csbabg  3133  cbvralcsf  3134  cbvrexcsf  3135  cbvreucsf  3136  dfss  3158  dfss2f  3161  ss2ab  3238  dfdif3  3260  difeqri  3270  ddifstab  3282  raldifb  3290  uneqri  3292  ssequn2  3323  unss  3324  rexun  3330  ralunb  3331  elin2  3338  ineqri  3343  dfss1  3354  dfss5  3355  dfss4st  3383  ssddif  3384  difin  3387  indif  3393  difundi  3402  indifdir  3406  symdifxor  3416  inrab2  3423  rabun2  3429  reuun2  3433  0el  3460  rabeq0  3467  abeq0  3468  disjr  3487  disj1  3488  undif4  3500  uneqdifeqim  3523  r19.2m  3524  r19.3rm  3526  r19.9rmv  3529  raaan  3544  pwss  3606  dfpr2  3626  rexdifpr  3635  ralsnsg  3644  ralsns  3645  eltpg  3652  eldiftp  3653  ralprg  3658  rexprg  3659  raltpg  3660  rextpg  3661  snprc  3672  rabrsndc  3675  euabsn2  3676  eusn  3681  eldifsn  3734  ssdifsn  3735  rexdifsn  3739  eqsnm  3770  tpss  3773  snsssn  3776  prel12  3786  preqsn  3790  oprcl  3817  pwtpss  3821  eluniab  3836  elunirab  3837  unipr  3838  dfnfc2  3842  uniun  3843  uniin  3844  uni0b  3849  unissb  3854  elintab  3870  elintrab  3871  ssintab  3876  ssintrab  3882  intun  3890  intpr  3891  elrint  3899  iuncom4  3908  iuneq2  3917  dfiun2g  3933  ssiinf  3951  iundif2ss  3967  elriin  3972  iunxiun  3983  pwssb  3987  elpwpw  3988  iunpwss  3993  dfdisj2  3997  disjiun  4013  cbvopab1  4091  dftr5  4119  trint  4131  inex1  4152  inuni  4173  repizf2lem  4179  unidif0  4185  axpweq  4189  bnd2  4191  exmid01  4216  zfpair2  4228  exss  4245  elop  4249  opm  4252  otth  4260  copsex4g  4265  opeqsn  4270  opelopabsbALT  4277  brabga  4282  opelopabaf  4291  iunopab  4299  pwunss  4301  pocl  4321  frirrg  4368  elsuci  4421  elsucg  4422  sucel  4428  unisucg  4432  uniuni  4469  reusv3  4478  iunpw  4498  setindel  4555  elirr  4558  en2lp  4571  ordpwsucss  4584  zfregfr  4591  tfi  4599  peano2  4612  peano5  4615  elxp  4661  opelxp  4674  brxp  4675  rabxp  4681  opthprc  4695  brab2a  4697  opeliunxp  4699  xpundi  4700  xpundir  4701  elvvv  4707  brinxp  4712  brab2ga  4719  0xp  4724  ssrel2  4734  eqrelrel  4745  reliun  4765  reluni  4767  raliunxp  4786  rexiunxp  4787  ralxpf  4791  rexxpf  4792  iunxpf  4793  relop  4795  elco  4811  elcnv  4822  elcnv2  4823  dmin  4853  dmuni  4855  dmopab  4856  dmi  4860  dmmrnm  4864  rnopab  4892  elrnmpt1  4896  rncoeq  4918  resiexg  4970  restidsing  4981  dfima2  4990  dfima3  4991  elima2  4994  elima3  4995  imai  5002  elimasn  5013  epini  5017  dfse2  5019  cotr  5028  issref  5029  intasym  5031  asymref  5032  cnvopab  5048  cnvi  5051  cnvdif  5053  imainss  5062  rnxpid  5081  dfrel2  5097  dfrel3  5104  dmsnm  5112  rnsnm  5113  relsn2m  5117  dmsnopg  5118  cnvcnvsn  5123  elxp4  5134  elxp5  5135  cnvresima  5136  mptpreima  5140  dfco2  5146  coundi  5148  coundir  5149  imaco  5152  coiun  5156  coi1  5162  relssdmrn  5167  relrelss  5173  unixpm  5182  ressn  5187  cnviinm  5188  cnvpom  5189  cnvsom  5190  cbviota  5201  iotass  5213  eliota  5223  dffun2  5245  dffun4  5246  dffun7  5262  dffun8  5263  dffun9  5264  funopab  5270  funun  5279  funcnvsn  5280  fntpg  5291  funcnv2  5295  funcnv  5296  fun2cnv  5299  fncnv  5301  fun11  5302  fununi  5303  imadiflem  5314  imadif  5315  imainlem  5316  funimaexglem  5318  fnunsn  5342  fnres  5351  fnopabg  5358  mptfng  5360  mptun  5366  fun  5407  fcnvres  5418  dff12  5439  f1cnvcnv  5451  funforn  5464  dff1o2  5485  dff1o5  5489  f1orn  5490  resdif  5502  ffoss  5512  f11o  5513  f1o00  5515  fo00  5516  elfv  5532  fv3  5557  nfvres  5568  eqfnfv3  5636  fneqeql  5645  unpreima  5662  respreima  5665  dffo3  5684  dffo5  5686  f1ompt  5688  ffnfvf  5696  fmptco  5703  ftpg  5721  fnressn  5723  idref  5778  abrexco  5781  dff13  5790  dff13f  5792  fliftel  5815  isoini  5840  eusvobj2  5883  acexmidlema  5888  acexmidlemb  5889  acexmidlemph  5890  acexmidlem2  5894  oprabid  5929  brabvv  5943  dfoprab2  5944  eqoprab2b  5955  dmoprab  5978  rnoprab  5980  eloprabga  5984  mpomptx  5988  resoprab  5993  ffnov  6001  elrnmpo  6011  ralrnmpo  6012  rexrnmpo  6013  ovid  6014  ovi3  6034  ov6g  6035  foov  6044  opabex3d  6147  opabex3  6148  abexssex  6151  oprabex3  6155  oprabrexex2  6156  fmpo  6227  xporderlem  6257  f1od2  6261  mpoxopovel  6267  brtpos2  6277  dmtpos  6282  tpostpos  6290  tpossym  6302  tposoprab  6306  dfsmo2  6313  tfrlem7  6343  tfrlem9  6345  tfr1onlemaccex  6374  tfrcllemaccex  6387  tfrcldm  6389  frecabex  6424  el1o  6463  dif1o  6464  dfer2  6561  brdifun  6587  eqerlem  6591  qsid  6627  iinerm  6634  riinerm  6635  erinxp  6636  brecop  6652  eroveu  6653  erovlem  6654  ecopovsym  6658  mapval2  6705  mapsn  6717  elixp  6732  ixpeq2  6739  ixpin  6750  ixpiinm  6751  mptelixpg  6761  ixpsnf1o  6763  domen  6778  isfi  6788  en1  6826  xpsnen  6848  xpcomco  6853  xpassen  6857  ssenen  6880  nneneq  6886  snnen2oprc  6889  ac6sfi  6927  exmidpw  6937  exmidpweq  6938  pw1dc1  6943  eldju  7098  djur  7099  eldju2ndl  7102  eldju2ndr  7103  finomni  7169  nninfwlporlemd  7201  nninfwlpoimlemg  7204  acfun  7237  pw1nel3  7261  sucpw1nel3  7263  ccfunen  7294  elni  7338  ltexpi  7367  enq0enq  7461  enq0ref  7463  enq0tr  7464  prarloclem3  7527  ltdfpr  7536  genpdflem  7537  genpassl  7554  genpassu  7555  nqprrnd  7573  nqprl  7581  nqpru  7582  ltexprlemopl  7631  ltexprlemopu  7633  ltexprlemdisj  7636  ltexprlemloc  7637  recexprlemdisj  7660  caucvgprprlemell  7715  caucvgprprlemelu  7716  suplocexprlemml  7746  suplocsrlemb  7836  opelcn  7856  elreal  7858  elreal2  7860  peano1nnnn  7882  axicn  7893  axaddf  7898  axmulf  7899  axprecex  7910  axpre-ltirr  7912  axpre-mulgt0  7917  axcaucvglemres  7929  axpre-suploc  7932  xrlenlt  8053  ltxrlt  8054  inelr  8572  reapcotr  8586  1nn  8961  elnnne0  9221  un0addcl  9240  un0mulcl  9241  elnnz  9294  elznn0nn  9298  elznn0  9299  elznn  9300  elz2  9355  zapne  9358  3halfnz  9381  prime  9383  raluz2  9611  rexuz2  9613  supinfneg  9627  infsupneg  9628  eluz2b2  9635  eluz2b3  9636  ublbneg  9645  elq  9654  qreccl  9674  elpq  9680  ralrp  9707  rexrp  9708  rpnegap  9718  ltxr  9807  xrnemnf  9809  xrltso  9828  icc0r  9958  divelunit  10034  fzprval  10114  fztpval  10115  elfz1b  10122  fz01or  10143  4fvwrd4  10172  fzolb  10185  fzolb2  10186  elfzo3  10195  fzouzsplit  10211  elfzo0z  10216  fzo0m  10223  fzind2  10271  ioo0  10292  ico0  10294  ioc0  10295  uzennn  10469  seq3f1olemp  10535  caucvgre  11025  cvg1nlemcau  11028  resqrexlemex  11069  climeu  11339  fsum2dlemstep  11477  expcnv  11547  prodsnf  11635  fprod2dlemstep  11665  divides  11831  m1exp1  11941  divalgb  11965  bezoutlemnewy  12032  bezoutlemmain  12034  bezoutlemex  12037  dfgcd2  12050  nnwosdc  12075  lcmgcdlem  12112  isprm2  12152  isprm3  12153  isprm4  12154  isprm5  12177  sqrt2irr  12197  oddpwdc  12209  pythagtriplem19  12317  pythagtrip  12318  pceu  12330  dvdsprmpweqnn  12371  4sqlem2  12424  4sqlem12  12437  ennnfoneleminc  12465  ennnfonelemex  12468  ennnfonelemr  12477  ctiunct  12494  infpn2  12510  xpsfrnel  12823  xpsfrnel2  12825  gsum0g  12874  ismnd  12895  dfgrp2e  12987  dfgrp3me  13059  isnsg2  13159  eqger  13180  isabl2  13250  imasabl  13290  isrhm  13525  isrim  13536  lss1d  13716  istps  14009  istps2  14010  isbasis2g  14022  tgval2  14028  txuni2  14233  tx1cn  14246  tx2cn  14247  uptx  14251  txdis1cn  14255  blres  14411  xmeterval  14412  xmeter  14413  isxms2  14429  isms2  14431  metrest  14483  qtopbasss  14498  dedekindicclemicc  14587  limcdifap  14608  pilem1  14677  sincosq1lem  14723  2sqlem1  14939  decidr  15026  bdcuni  15106  bdcriota  15113  bdinex1  15129  bj-zfpair2  15140  bj-axun2  15145  bj-ssom  15166  ss1oel2o  15222  nninfsellemdc  15238  nninfsellemsuc  15240  nninfsellemqall  15243  trirec0xor  15272  iswomni0  15278