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  1946  eean  1947  sbn  1968  sbim  1969  sbor  1970  sban  1971  sbrim  1972  sblim  1973  sbbi  1975  sblbis  1976  sbrbis  1977  sbrbif  1978  sbco2d  1982  sbco2vd  1983  sbnf2  1997  2sb5  1999  2sb6  2000  sbcom2v  2001  sbcom2v2  2002  sbcom2  2003  sb6a  2004  2sb5rf  2005  2sb6rf  2006  sbalyz  2015  sbal  2016  sbal1yz  2017  sbex  2020  sbalv  2021  sbco4lem  2022  exsb  2024  2exsb  2025  eujust  2044  euf  2047  cbveu  2066  mor  2084  eu2  2086  mo4f  2102  eu4  2104  2exeu  2134  2eu4  2135  exists1  2138  abid  2181  eleq12i  2261  abeq2  2302  abeq2i  2304  clabel  2320  abid2f  2362  sbabel  2363  neeq12i  2381  neanior  2451  ralnex  2482  dfrex2dc  2485  ralinexa  2521  nfraldya  2529  nfrexdya  2530  r3al  2538  r19.26-2  2623  ralbiim  2628  ralnex2  2633  r19.43  2652  ralcomf  2655  rexcomf  2656  ralrot3  2659  rexrot4  2661  reean  2663  3reeanv  2665  rabbi  2672  cbvralf  2718  cbvrexf  2719  cbvreu  2724  cbvral2vw  2737  cbvrex2vw  2738  cbvral2v  2739  cbvrex2v  2740  cbvral3v  2741  cbvralsv  2742  cbvrexsv  2743  sbralie  2744  rabeq2i  2757  issetf  2767  2gencl  2793  3gencl  2794  ceqsex2  2801  ceqsex3v  2803  ceqsex6v  2805  ceqsex8v  2806  gencbvex  2807  gencbval  2809  spc2gv  2852  eqvincf  2886  ceqsrex2v  2893  clel5  2898  elrab2  2920  ralab  2921  ralrab  2922  rexab  2923  rexrab  2924  ralab2  2925  rexab2  2927  eueq3dc  2935  morex  2945  euind  2948  reu2  2949  reu6  2950  rmo4  2954  reu4  2955  reu7  2956  rmo3f  2958  rmo4f  2959  rmoim  2962  2reuswapdc  2965  reuind  2966  2rmorex  2967  sbcco  3008  sbccomlem  3061  sbccom  3062  ra5  3075  rmo3  3078  csbco  3091  csbcow  3092  sbnfc2  3142  csbabg  3143  cbvralcsf  3144  cbvrexcsf  3145  cbvreucsf  3146  dfss  3168  dfss2f  3171  ss2ab  3248  dfdif3  3270  difeqri  3280  ddifstab  3292  raldifb  3300  uneqri  3302  ssequn2  3333  unss  3334  rexun  3340  ralunb  3341  elin2  3348  ineqri  3353  dfss1  3364  dfss5  3365  dfss4st  3393  ssddif  3394  difin  3397  indif  3403  difundi  3412  indifdir  3416  symdifxor  3426  inrab2  3433  rabun2  3439  reuun2  3443  0el  3470  rabeq0  3477  abeq0  3478  disjr  3497  disj1  3498  undif4  3510  uneqdifeqim  3533  r19.2m  3534  r19.3rm  3536  r19.9rmv  3539  raaan  3553  pwss  3618  dfpr2  3638  rexdifpr  3647  ralsnsg  3656  ralsns  3657  eltpg  3664  eldiftp  3665  ralprg  3670  rexprg  3671  raltpg  3672  rextpg  3673  snprc  3684  rabrsndc  3687  euabsn2  3688  eusn  3693  eldifsn  3746  ssdifsn  3747  rexdifsn  3751  eqsnm  3782  tpss  3785  snsssn  3788  prel12  3798  preqsn  3802  oprcl  3829  pwtpss  3833  eluniab  3848  elunirab  3849  unipr  3850  dfnfc2  3854  uniun  3855  uniin  3856  uni0b  3861  unissb  3866  elintab  3882  elintrab  3883  ssintab  3888  ssintrab  3894  intun  3902  intpr  3903  elrint  3911  iuncom4  3920  iuneq2  3929  dfiun2g  3945  ssiinf  3963  iundif2ss  3979  elriin  3984  iunxiun  3995  pwssb  3999  elpwpw  4000  iunpwss  4005  dfdisj2  4009  disjiun  4025  cbvopab1  4103  dftr5  4131  trint  4143  inex1  4164  inuni  4185  repizf2lem  4191  unidif0  4197  axpweq  4201  bnd2  4203  exmid01  4228  zfpair2  4240  exss  4257  elop  4261  opm  4264  otth  4272  copsex4g  4277  opeqsn  4282  opelopabsbALT  4290  brabga  4295  opelopabaf  4305  iunopab  4313  pwunss  4315  pocl  4335  frirrg  4382  elsuci  4435  elsucg  4436  sucel  4442  unisucg  4446  uniuni  4483  reusv3  4492  iunpw  4512  setindel  4571  elirr  4574  en2lp  4587  ordpwsucss  4600  zfregfr  4607  tfi  4615  peano2  4628  peano5  4631  elxp  4677  opelxp  4690  brxp  4691  rabxp  4697  opthprc  4711  brab2a  4713  opeliunxp  4715  xpundi  4716  xpundir  4717  elvvv  4723  brinxp  4728  brab2ga  4735  0xp  4740  ssrel2  4750  eqrelrel  4761  reliun  4781  reluni  4783  raliunxp  4804  rexiunxp  4805  ralxpf  4809  rexxpf  4810  iunxpf  4811  relop  4813  elco  4829  elcnv  4840  elcnv2  4841  dmin  4871  dmuni  4873  dmopab  4874  dmi  4878  dmmrnm  4882  rnopab  4910  elrnmpt1  4914  rncoeq  4936  resiexg  4988  restidsing  4999  dfima2  5008  dfima3  5009  elima2  5012  elima3  5013  imai  5022  elimasn  5033  epini  5037  dfse2  5039  cotr  5048  issref  5049  intasym  5051  asymref  5052  cnvopab  5068  cnvi  5071  cnvdif  5073  imainss  5082  rnxpid  5101  dfrel2  5117  dfrel3  5124  dmsnm  5132  rnsnm  5133  relsn2m  5137  dmsnopg  5138  cnvcnvsn  5143  elxp4  5154  elxp5  5155  cnvresima  5156  mptpreima  5160  dfco2  5166  coundi  5168  coundir  5169  imaco  5172  coiun  5176  coi1  5182  relssdmrn  5187  relrelss  5193  unixpm  5202  ressn  5207  cnviinm  5208  cnvpom  5209  cnvsom  5210  cbviota  5221  iotass  5233  eliota  5243  dffun2  5265  dffun4  5266  dffun7  5282  dffun8  5283  dffun9  5284  funopab  5290  funun  5299  funcnvsn  5300  fntpg  5311  funcnv2  5315  funcnv  5316  fun2cnv  5319  fncnv  5321  fun11  5322  fununi  5323  imadiflem  5334  imadif  5335  imainlem  5336  funimaexglem  5338  fnunsn  5362  fnres  5371  fnopabg  5378  mptfng  5380  mptun  5386  fun  5427  fcnvres  5438  dff12  5459  f1cnvcnv  5471  funforn  5484  dff1o2  5506  dff1o5  5510  f1orn  5511  resdif  5523  ffoss  5533  f11o  5534  f1o00  5536  fo00  5537  elfv  5553  fv3  5578  nfvres  5589  eqfnfv3  5658  fneqeql  5667  unpreima  5684  respreima  5687  dffo3  5706  dffo5  5708  f1ompt  5710  ffnfvf  5718  fmptco  5725  ftpg  5743  fnressn  5745  idref  5800  abrexco  5803  dff13  5812  dff13f  5814  fliftel  5837  isoini  5862  eusvobj2  5905  acexmidlema  5910  acexmidlemb  5911  acexmidlemph  5912  acexmidlem2  5916  oprabid  5951  brabvv  5965  dfoprab2  5966  eqoprab2b  5977  dmoprab  6000  rnoprab  6002  eloprabga  6006  mpomptx  6010  resoprab  6015  ffnov  6023  elrnmpo  6033  ralrnmpo  6034  rexrnmpo  6035  ovid  6036  ovi3  6057  ov6g  6058  foov  6067  opabex3d  6175  opabex3  6176  abexssex  6179  oprabex3  6183  oprabrexex2  6184  fmpo  6256  xporderlem  6286  f1od2  6290  mpoxopovel  6296  brtpos2  6306  dmtpos  6311  tpostpos  6319  tpossym  6331  tposoprab  6335  dfsmo2  6342  tfrlem7  6372  tfrlem9  6374  tfr1onlemaccex  6403  tfrcllemaccex  6416  tfrcldm  6418  frecabex  6453  el1o  6492  dif1o  6493  dfer2  6590  brdifun  6616  eqerlem  6620  qsid  6656  iinerm  6663  riinerm  6664  erinxp  6665  brecop  6681  eroveu  6682  erovlem  6683  ecopovsym  6687  mapval2  6734  mapsn  6746  elixp  6761  ixpeq2  6768  ixpin  6779  ixpiinm  6780  mptelixpg  6790  ixpsnf1o  6792  domen  6807  isfi  6817  en1  6855  xpsnen  6877  xpcomco  6882  xpassen  6886  ssenen  6909  nneneq  6915  snnen2oprc  6918  ac6sfi  6956  exmidpw  6966  exmidpweq  6967  pw1dc1  6972  eldju  7129  djur  7130  eldju2ndl  7133  eldju2ndr  7134  finomni  7201  nninfwlporlemd  7233  nninfwlpoimlemg  7236  acfun  7269  pw1nel3  7293  sucpw1nel3  7295  ccfunen  7326  elni  7370  ltexpi  7399  enq0enq  7493  enq0ref  7495  enq0tr  7496  prarloclem3  7559  ltdfpr  7568  genpdflem  7569  genpassl  7586  genpassu  7587  nqprrnd  7605  nqprl  7613  nqpru  7614  ltexprlemopl  7663  ltexprlemopu  7665  ltexprlemdisj  7668  ltexprlemloc  7669  recexprlemdisj  7692  caucvgprprlemell  7747  caucvgprprlemelu  7748  suplocexprlemml  7778  suplocsrlemb  7868  opelcn  7888  elreal  7890  elreal2  7892  peano1nnnn  7914  axicn  7925  axaddf  7930  axmulf  7931  axprecex  7942  axpre-ltirr  7944  axpre-mulgt0  7949  axcaucvglemres  7961  axpre-suploc  7964  xrlenlt  8086  ltxrlt  8087  inelr  8605  reapcotr  8619  1nn  8995  elnnne0  9257  un0addcl  9276  un0mulcl  9277  elnnz  9330  elznn0nn  9334  elznn0  9335  elznn  9336  elz2  9391  zapne  9394  3halfnz  9417  prime  9419  raluz2  9647  rexuz2  9649  supinfneg  9663  infsupneg  9664  eluz2b2  9671  eluz2b3  9672  ublbneg  9681  elq  9690  qreccl  9710  elpq  9717  ralrp  9744  rexrp  9745  rpnegap  9755  ltxr  9844  xrnemnf  9846  xrltso  9865  icc0r  9995  divelunit  10071  fzprval  10151  fztpval  10152  elfz1b  10159  fz01or  10180  4fvwrd4  10209  fzolb  10223  fzolb2  10224  elfzo3  10233  fzouzsplit  10249  elfzo0z  10254  fzo0m  10261  fzind2  10309  ioo0  10331  ico0  10333  ioc0  10334  uzennn  10510  seq3f1olemp  10589  iswrd  10919  caucvgre  11128  cvg1nlemcau  11131  resqrexlemex  11172  climeu  11442  fsum2dlemstep  11580  expcnv  11650  prodsnf  11738  fprod2dlemstep  11768  divides  11935  m1exp1  12045  divalgb  12069  bezoutlemnewy  12136  bezoutlemmain  12138  bezoutlemex  12141  dfgcd2  12154  nnwosdc  12179  lcmgcdlem  12218  isprm2  12258  isprm3  12259  isprm4  12260  isprm5  12283  sqrt2irr  12303  oddpwdc  12315  pythagtriplem19  12423  pythagtrip  12424  pceu  12436  dvdsprmpweqnn  12477  4sqlem2  12530  4sqlem12  12543  ennnfoneleminc  12571  ennnfonelemex  12574  ennnfonelemr  12583  ctiunct  12600  infpn2  12616  xpsfrnel  12930  xpsfrnel2  12932  gsum0g  12982  ismnd  13003  dfgrp2e  13103  dfgrp3me  13175  isnsg2  13276  eqger  13297  isabl2  13367  imasabl  13409  isrhm  13657  isrim  13668  isnzr2  13683  lss1d  13882  istps  14211  istps2  14212  isbasis2g  14224  tgval2  14230  txuni2  14435  tx1cn  14448  tx2cn  14449  uptx  14453  txdis1cn  14457  blres  14613  xmeterval  14614  xmeter  14615  isxms2  14631  isms2  14633  metrest  14685  qtopbasss  14700  dedekindicclemicc  14811  limcdifap  14841  plyrecj  14941  pilem1  14955  sincosq1lem  15001  gausslemma2dlem1a  15215  gausslemma2dlem4  15221  lgsquadlem1  15234  lgsquadlem2  15235  2lgslem1b  15246  2sqlem1  15271  decidr  15358  bdcuni  15438  bdcriota  15445  bdinex1  15461  bj-zfpair2  15472  bj-axun2  15477  bj-ssom  15498  ss1oel2o  15554  nninfsellemdc  15570  nninfsellemsuc  15572  nninfsellemqall  15575  trirec0xor  15605  iswomni0  15611