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  394  biadan2  460  anbi2ci  463  anbi12i  464  anbi12ci  465  bianassc  474  pm5.3  479  an42  593  xchbinx  693  mt2bi  695  orbi12i  776  or42  784  pm5.53  814  orddi  832  anddi  833  pm2.1dc  849  dcim  853  notnotrdc  855  dcnnOLD  861  rbaib  933  rbaibr  934  pm4.43  962  orbididc  966  pm5.75  975  ifptru  1002  ifpfal  1003  3orass  1012  3anass  1013  3ancomb  1017  3anan32  1020  3anan12  1021  anandi3  1022  anandi3r  1023  xordc  1441  falbitru  1466  19.26-2  1535  19.26-3an  1536  alrot3  1538  albiim  1540  2albiim  1541  19.27h  1613  19.27  1614  19.28h  1615  19.28  1616  nfalt  1631  aaanh  1639  aaan  1640  alinexa  1656  19.21-2  1719  nf2  1720  19.44  1734  19.45  1735  exrot3  1742  exrot4  1743  eeor  1747  sbcof2  1863  sbid2h  1902  19.23vv  1937  sbnv  1943  sblimv  1950  pm11.53  1951  19.41vv  1959  19.41vvv  1960  19.41vvvv  1961  exdistrv  1966  19.42vv  1967  19.42vvv  1968  19.42vvvv  1969  4exdistr  1972  cbvex4v  1990  eean  1991  sbn  2012  sbim  2013  sbor  2014  sban  2015  sbrim  2016  sblim  2017  sbbi  2019  sblbis  2020  sbrbis  2021  sbrbif  2022  sbco2d  2026  sbco2vd  2027  sbnf2  2041  2sb5  2043  2sb6  2044  sbcom2v  2045  sbcom2v2  2046  sbcom2  2047  sb6a  2048  2sb5rf  2049  2sb6rf  2050  sbalyz  2059  sbal  2060  sbal1yz  2061  sbex  2064  sbalv  2065  sbco4lem  2066  exsb  2068  2exsb  2069  eujust  2088  euf  2091  cbveu  2110  mor  2129  eu2  2131  mo4f  2147  eu4  2149  2exeu  2179  2eu4  2180  exists1  2183  abid  2226  eleq12i  2306  abeq2  2347  abeq2i  2349  abbib  2356  clabel  2367  eqabb  2374  eqabbw  2375  abid2f  2418  sbabel  2419  neeq12i  2437  neanior  2507  ralnex  2538  dfrex2dc  2541  ralinexa  2577  nfraldya  2585  nfrexdya  2586  r3al  2594  r19.26-2  2680  ralbiim  2685  ralnex2  2690  r19.43  2709  ralcomf  2712  rexcomf  2713  ralrot3  2716  rexrot4  2718  reean  2720  3reeanv  2722  reqabi  2728  rabbi  2730  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvral2vw  2797  cbvrex2vw  2798  cbvral2v  2799  cbvrex2v  2800  cbvral3v  2801  cbvralsv  2802  cbvrexsv  2803  sbralie  2804  rabeq2i  2818  issetf  2829  2gencl  2855  3gencl  2856  ceqsex2  2863  ceqsex3v  2865  ceqsex6v  2867  ceqsex8v  2868  gencbvex  2869  gencbval  2871  spc2gv  2916  eqvincf  2951  ceqsrex2v  2958  clel5  2963  elrab2  2985  ralab  2986  ralrab  2987  rexab  2988  rexrab  2989  ralab2  2990  rexab2  2992  eueq3dc  3000  morex  3010  euind  3013  reu2  3014  reu6  3015  rmo4  3019  reu4  3020  reu7  3021  rmo3f  3023  rmo4f  3024  rmoim  3027  2reuswapdc  3030  reuind  3031  2rmorex  3032  sbcco  3073  sbccomlem  3126  sbccom  3127  ra5  3141  rmo3  3144  csbco  3157  csbcow  3158  sbnfc2  3208  csbabg  3209  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  dfss  3234  dfssf  3238  dfss2f  3239  ss2ab  3316  dfdif3  3339  difeqri  3349  ddifstab  3361  raldifb  3369  uneqri  3371  ssequn2  3402  unss  3403  rexun  3409  ralunb  3410  elin2  3417  ineqri  3424  dfss1  3435  dfss5  3436  dfss4st  3464  ssddif  3465  difin  3468  indif  3474  difundi  3483  indifdir  3487  symdifxor  3497  inrab2  3506  rabun2  3512  reuun2  3516  0el  3544  ab0w  3550  rabeq0  3552  abeq0  3553  disjr  3573  disj1  3574  undif4  3586  uneqdifeqim  3610  r19.2m  3611  r19.3rm  3613  r19.9rmv  3616  raaan  3630  pwss  3704  dfpr2  3724  rexdifpr  3733  ralsnsg  3742  ralsns  3743  eltpg  3750  eldiftp  3751  ralprg  3756  rexprg  3757  raltpg  3758  rextpg  3759  snprc  3770  rabrsndc  3775  euabsn2  3776  eusn  3781  eldifsn  3836  ssdifsn  3837  rexdifsn  3841  eqsnm  3875  tpss  3878  snsssn  3881  prel12  3891  preqsn  3895  oprcl  3923  pwtpss  3927  eluniab  3942  elunirab  3943  unipr  3944  dfnfc2  3948  uniun  3949  uniin  3950  uni0b  3955  unissb  3960  elintab  3976  elintrab  3977  ssintab  3982  ssintrab  3988  intun  3996  intpr  3997  elrint  4005  iuncom4  4014  iuneq2  4023  dfiun2g  4039  ssiinf  4057  iundif2ss  4073  elriin  4078  iunxiun  4089  pwssb  4093  elpwpw  4094  iunpwss  4099  dfdisj2  4103  disjiun  4120  cbvopab1  4199  dftr5  4227  trint  4239  inex1  4262  inuni  4286  repizf2lem  4293  unidif0  4299  axpweq  4303  bnd2  4305  exmid01  4330  zfpair2  4342  exss  4362  elop  4366  opm  4369  otth  4377  copsex4g  4382  opeqsn  4388  opelopabsbALT  4396  brabga  4401  opelopabaf  4411  iunopab  4419  pwunss  4423  pocl  4443  frirrg  4490  elsuci  4543  elsucg  4544  sucel  4550  unisucg  4554  uniuni  4592  reusv3  4601  iunpw  4621  setindel  4680  elirr  4683  en2lp  4696  ordpwsucss  4709  zfregfr  4716  tfi  4724  peano2  4737  peano5  4740  elxp  4786  opelxp  4799  brxp  4800  rabxp  4807  opthprc  4821  brab2a  4823  opeliunxp  4825  xpundi  4826  xpundir  4827  elvvv  4833  brinxp  4838  brab2ga  4845  0xp  4850  ssrel2  4860  eqrelrel  4871  reliun  4893  reluni  4895  raliunxp  4916  rexiunxp  4917  ralxpf  4921  rexxpf  4922  iunxpf  4923  relop  4925  elco  4941  elcnv  4952  elcnv2  4953  dmin  4984  dmuni  4986  dmopab  4987  dmi  4991  dmmrnm  4996  rnopab  5024  elrnmpt1  5028  rncoeq  5051  resiexg  5103  restidsing  5114  dfima2  5123  dfima3  5124  elima2  5127  elima3  5128  imai  5138  elimasn  5149  epini  5153  dfse2  5155  cotr  5164  issref  5165  intasym  5167  asymref  5168  cnvopab  5184  cnvi  5187  cnvdif  5189  imainss  5198  rnxpid  5217  dfrel2  5233  dfrel3  5240  dmsnm  5248  rnsnm  5249  relsn2m  5253  dmsnopg  5254  cnvcnvsn  5259  elxp4  5270  elxp5  5271  cnvresima  5272  mptpreima  5276  dfco2  5282  coundi  5284  coundir  5285  imaco  5288  coiun  5292  coi1  5298  relssdmrn  5303  relrelss  5309  unixpm  5318  ressn  5323  cnviinm  5324  cnvpom  5325  cnvsom  5326  cbviota  5337  iotass  5350  eliota  5360  dffun2  5382  dffun4  5383  dffun7  5399  dffun8  5400  dffun9  5401  funopab  5407  funun  5417  funcnvsn  5421  fntpg  5432  funcnv2  5436  funcnv  5437  fun2cnv  5440  fncnv  5442  fun11  5443  fununi  5444  imadiflem  5455  imadif  5456  imainlem  5457  funimaexglem  5459  fnunsn  5485  fnres  5495  fnopabg  5502  mptfng  5504  mptun  5510  fun  5556  fcnvres  5570  dff12  5592  f1cnvcnv  5604  funforn  5617  dff1o2  5639  dff1o5  5643  f1orn  5644  resdif  5656  ffoss  5667  f11o  5668  f1o00  5671  fo00  5672  elfv  5688  fv3  5713  nfvres  5726  eqfnfv3  5799  fneqeql  5808  unpreima  5824  respreima  5827  dffo3  5846  dffo5  5848  f1ompt  5850  ffnfvf  5858  fmptco  5865  funopdmsn  5886  ftpg  5890  fnressn  5892  idref  5952  abrexco  5955  dff13  5964  dff13f  5966  fliftel  5989  isoini  6014  eusvobj2  6061  acexmidlema  6066  acexmidlemb  6067  acexmidlemph  6068  acexmidlem2  6072  oprabid  6107  brabvv  6124  dfoprab2  6125  eqoprab2b  6136  dmoprab  6159  rnoprab  6161  eloprabga  6165  mpomptx  6169  resoprab  6174  ffnov  6182  elrnmpo  6192  ralrnmpo  6193  rexrnmpo  6194  ovid  6195  ovi3  6216  ov6g  6217  foov  6226  opabex3d  6340  opabex3  6341  abexssex  6344  oprabex3  6352  oprabrexex2  6353  fmpo  6427  xporderlem  6457  f1od2  6461  mpoxopovel  6502  brtpos2  6512  dmtpos  6517  tpostpos  6525  tpossym  6537  tposoprab  6541  dfsmo2  6548  tfrlem7  6578  tfrlem9  6580  tfr1onlemaccex  6609  tfrcllemaccex  6622  tfrcldm  6624  frecabex  6659  el1o  6700  dif1o  6701  dfer2  6798  brdifun  6824  eqerlem  6828  qsid  6864  iinerm  6871  riinerm  6872  erinxp  6873  brecop  6889  eroveu  6890  erovlem  6891  ecopovsym  6895  mapval2  6949  mapsn  6962  elixp  6977  ixpeq2  6984  ixpin  6995  ixpiinm  6996  mptelixpg  7006  ixpsnf1o  7008  domen  7025  isfi  7037  en1  7076  modom2  7099  xpsnen  7109  xpcomco  7114  xpassen  7118  ssenen  7142  nneneq  7148  snnen2oprc  7151  ac6sfi  7192  exmidpw  7205  exmidpweq  7206  pw1dc1  7211  elfpw  7252  eldju  7398  djur  7399  eldju2ndl  7402  eldju2ndr  7403  finomni  7470  nninfwlporlemd  7502  nninfwlpoimlemg  7505  acfun  7553  pw1nel3  7580  sucpw1nel3  7582  ccfunen  7620  elni  7665  ltexpi  7694  enq0enq  7788  enq0ref  7790  enq0tr  7791  prarloclem3  7854  ltdfpr  7863  genpdflem  7864  genpassl  7881  genpassu  7882  nqprrnd  7900  nqprl  7908  nqpru  7909  ltexprlemopl  7958  ltexprlemopu  7960  ltexprlemdisj  7963  ltexprlemloc  7964  recexprlemdisj  7987  caucvgprprlemell  8042  caucvgprprlemelu  8043  suplocexprlemml  8073  suplocsrlemb  8163  opelcn  8183  elreal  8185  elreal2  8187  peano1nnnn  8209  axicn  8220  axaddf  8225  axmulf  8226  axprecex  8237  axpre-ltirr  8239  axpre-mulgt0  8244  axcaucvglemres  8256  axpre-suploc  8259  xrlenlt  8380  ltxrlt  8381  inelr  8902  reapcotr  8916  1nn  9294  elnnne0  9556  un0addcl  9575  un0mulcl  9576  elnnz  9633  elznn0nn  9637  elznn0  9638  elznn  9639  elz2  9695  zapne  9698  3halfnz  9722  prime  9724  raluz2  9958  rexuz2  9960  supinfneg  9974  infsupneg  9975  eluz2b2  9982  eluz2b3  9983  ublbneg  9992  elq  10001  qreccl  10021  elpq  10028  ralrp  10055  rexrp  10056  rpnegap  10066  ltxr  10156  xrnemnf  10158  xrltso  10177  icc0r  10307  divelunit  10383  fzprval  10467  fztpval  10468  elfz1b  10475  fz01or  10496  4fvwrd4  10525  fzolb  10539  fzolb2  10540  elfzo3  10549  fzouzsplit  10566  elfzo0z  10574  fzo0m  10582  fzind2  10636  infssfzcldc  10647  infssfzledc  10648  ioo0  10672  ico0  10674  ioc0  10675  uzennn  10851  seq3f1olemp  10930  sseqn  11257  hashfibc  11261  hashf1lem2  11264  iswrd  11284  caucvgre  11725  cvg1nlemcau  11728  resqrexlemex  11769  climeu  12040  fsum2dlemstep  12179  expcnv  12249  prodsnf  12337  fprod2dlemstep  12367  divides  12534  m1exp1  12646  divalgb  12670  bitsval2  12689  bitsmod  12701  bitscmp  12703  bezoutlemnewy  12751  bezoutlemmain  12753  bezoutlemex  12756  dfgcd2  12769  nnwosdc  12794  lcmgcdlem  12833  isprm2  12873  isprm3  12874  isprm4  12875  isprm5  12898  sqrt2irr  12918  oddpwdc  12930  pythagtriplem19  13039  pythagtrip  13040  pceu  13052  dvdsprmpweqnn  13093  4sqlem2  13146  4sqlem12  13159  dec5dvds2  13170  ballotfilemodife  13218  ballotfilem4  13219  ennnfoneleminc  13280  ennnfonelemex  13283  ennnfonelemr  13292  ctiunct  13309  infpn2  13325  xpsfrnel  13642  xpsfrnel2  13644  gzsum0  13690  ismnd  13709  dfgrp2e  13810  dfgrp3me  13882  isnsg2  13983  eqger  14004  isabl2  14074  imasabl  14117  isrhm  14438  isrim  14449  isnzr2  14464  drngprop  14590  lss1d  14692  istps  15056  istps2  15057  isbasis2g  15069  tgval2  15075  txuni2  15280  tx1cn  15293  tx2cn  15294  uptx  15298  txdis1cn  15302  blres  15458  xmeterval  15459  xmeter  15460  isxms2  15476  isms2  15478  metrest  15530  qtopbasss  15545  dedekindicclemicc  15656  limcdifap  15686  plyrecj  15787  pilem1  15803  sincosq1lem  15849  mpodvdsmulf1o  16018  gausslemma2dlem1a  16091  gausslemma2dlem4  16097  lgsquadlem1  16110  lgsquadlem2  16111  2lgslem1b  16122  2sqlem1  16147  upgrex  16258  griedg0ssusgr  16406  clwwlkn1loopb  16575  clwwlknon2x  16590  decidr  16738  bdcuni  16816  bdcriota  16823  bdinex1  16839  bj-zfpair2  16850  bj-axun2  16855  bj-ssom  16876  ss1oel2o  16931  nninfsellemdc  16958  nninfsellemsuc  16960  nninfsellemqall  16963  trirec0xor  16999  iswomni0  17006