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 )

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3574  disj1  3575  undif4  3587  uneqdifeqim  3613  r19.2m  3614  r19.3rm  3616  r19.9rmv  3619  raaan  3633  pwss  3708  dfpr2  3728  rexdifpr  3737  ralsnsg  3746  ralsns  3747  eltpg  3754  eldiftp  3755  ralprg  3760  rexprg  3761  raltpg  3762  rextpg  3763  snprc  3774  rabrsndc  3779  euabsn2  3780  eusn  3785  eldifsn  3841  ssdifsn  3842  rexdifsn  3846  eqsnm  3880  tpss  3883  snsssn  3886  prel12  3896  preqsn  3900  oprcl  3928  pwtpss  3932  eluniab  3947  elunirab  3948  unipr  3949  dfnfc2  3953  uniun  3954  uniin  3955  uni0b  3960  unissb  3965  elintab  3981  elintrab  3982  ssintab  3987  ssintrab  3993  intun  4001  intpr  4002  elrint  4010  iuncom4  4019  iuneq2  4028  dfiun2g  4044  ssiinf  4062  iundif2ss  4078  elriin  4083  iunxiun  4094  pwssb  4098  elpwpw  4099  iunpwss  4104  dfdisj2  4108  disjiun  4125  cbvopab1  4204  dftr5  4232  trint  4244  inex1  4267  inuni  4291  repizf2lem  4298  unidif0  4304  axpweq  4308  bnd2  4310  exmid01  4335  zfpair2  4347  exss  4367  elop  4371  opm  4374  otth  4382  copsex4g  4387  opeqsn  4393  opelopabsbALT  4401  brabga  4406  opelopabaf  4416  iunopab  4424  pwunss  4428  pocl  4448  frirrg  4495  elsuci  4548  elsucg  4549  sucel  4555  unisucg  4559  uniuni  4597  reusv3  4606  iunpw  4626  setindel  4685  elirr  4688  en2lp  4701  ordpwsucss  4714  zfregfr  4721  tfi  4729  peano2  4742  peano5  4745  elxp  4791  opelxp  4804  brxp  4805  rabxp  4812  opthprc  4826  brab2a  4828  opeliunxp  4830  xpundi  4831  xpundir  4832  elvvv  4838  brinxp  4843  brab2ga  4850  0xp  4855  ssrel2  4865  eqrelrel  4876  reliun  4898  reluni  4900  raliunxp  4921  rexiunxp  4922  ralxpf  4926  rexxpf  4927  iunxpf  4928  relop  4930  elco  4946  elcnv  4957  elcnv2  4958  dmin  4989  dmuni  4991  dmopab  4992  dmi  4996  dmmrnm  5001  rnopab  5029  elrnmpt1  5033  rncoeq  5056  resiexg  5108  restidsing  5119  dfima2  5128  dfima3  5129  elima2  5132  elima3  5133  imai  5143  elimasn  5154  epini  5158  dfse2  5160  cotr  5169  issref  5170  intasym  5172  asymref  5173  cnvopab  5189  cnvi  5192  cnvdif  5194  imainss  5203  rnxpid  5222  dfrel2  5238  dfrel3  5245  dmsnm  5253  rnsnm  5254  relsn2m  5258  dmsnopg  5259  cnvcnvsn  5264  elxp4  5275  elxp5  5276  cnvresima  5277  mptpreima  5281  dfco2  5287  coundi  5289  coundir  5290  imaco  5293  coiun  5297  coi1  5303  relssdmrn  5308  relrelss  5314  unixpm  5323  ressn  5328  cnviinm  5329  cnvpom  5330  cnvsom  5331  cbviota  5342  iotass  5355  eliota  5365  dffun2  5387  dffun4  5388  dffun7  5404  dffun8  5405  dffun9  5406  funopab  5412  funun  5422  funcnvsn  5426  fntpg  5437  funcnv2  5441  funcnv  5442  fun2cnv  5445  fncnv  5447  fun11  5448  fununi  5449  imadiflem  5460  imadif  5461  imainlem  5462  funimaexglem  5464  fnunsn  5490  fnres  5500  fnopabg  5507  mptfng  5509  mptun  5515  fun  5561  fcnvres  5575  dff12  5597  f1cnvcnv  5609  funforn  5622  dff1o2  5644  dff1o5  5648  f1orn  5649  resdif  5661  ffoss  5672  f11o  5673  f1o00  5676  fo00  5677  elfv  5693  fv3  5718  nfvres  5732  eqfnfv3  5808  fneqeql  5817  unpreima  5833  respreima  5836  dffo3  5855  dffo5  5857  f1ompt  5859  ffnfvf  5867  fmptco  5874  funopdmsn  5895  ftpg  5899  fnressn  5901  idref  5962  abrexco  5965  dff13  5974  dff13f  5976  fliftel  5999  isoini  6024  eusvobj2  6071  acexmidlema  6076  acexmidlemb  6077  acexmidlemph  6078  acexmidlem2  6082  oprabid  6117  brabvv  6134  dfoprab2  6135  eqoprab2b  6146  dmoprab  6169  rnoprab  6171  eloprabga  6175  mpomptx  6179  resoprab  6184  ffnov  6192  elrnmpo  6202  ralrnmpo  6203  rexrnmpo  6204  ovid  6205  ovi3  6226  ov6g  6227  foov  6236  opabex3d  6350  opabex3  6351  abexssex  6354  oprabex3  6362  oprabrexex2  6363  fmpo  6437  xporderlem  6467  f1od2  6471  mpoxopovel  6512  brtpos2  6522  dmtpos  6527  tpostpos  6535  tpossym  6547  tposoprab  6551  dfsmo2  6558  tfrlem7  6588  tfrlem9  6590  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfrcldm  6634  frecabex  6669  el1o  6710  dif1o  6711  dfer2  6808  brdifun  6834  eqerlem  6838  qsid  6874  iinerm  6881  riinerm  6882  erinxp  6883  brecop  6899  eroveu  6900  erovlem  6901  ecopovsym  6905  mapval2  6959  mapsn  6972  elixp  6987  ixpeq2  6994  ixpin  7005  ixpiinm  7006  mptelixpg  7016  ixpsnf1o  7018  domen  7035  isfi  7047  en1  7086  modom2  7109  xpsnen  7119  xpcomco  7124  xpassen  7128  ssenen  7152  nneneq  7158  snnen2oprc  7161  ac6sfi  7202  exmidpw  7215  exmidpweq  7216  pw1dc1  7221  elfpw  7262  eldju  7408  djur  7409  eldju2ndl  7412  eldju2ndr  7413  finomni  7480  nninfwlporlemd  7512  nninfwlpoimlemg  7515  acfun  7563  pw1nel3  7590  sucpw1nel3  7592  ccfunen  7630  elni  7675  ltexpi  7704  enq0enq  7798  enq0ref  7800  enq0tr  7801  prarloclem3  7864  ltdfpr  7873  genpdflem  7874  genpassl  7891  genpassu  7892  nqprrnd  7910  nqprl  7918  nqpru  7919  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemdisj  7973  ltexprlemloc  7974  recexprlemdisj  7997  caucvgprprlemell  8052  caucvgprprlemelu  8053  suplocexprlemml  8083  suplocsrlemb  8173  opelcn  8193  elreal  8195  elreal2  8197  peano1nnnn  8219  axicn  8230  axaddf  8235  axmulf  8236  axprecex  8247  axpre-ltirr  8249  axpre-mulgt0  8254  axcaucvglemres  8266  axpre-suploc  8269  xrlenlt  8390  ltxrlt  8391  inelr  8912  reapcotr  8926  1nn  9315  elnnne0  9577  un0addcl  9596  un0mulcl  9597  elnnz  9654  elznn0nn  9658  elznn0  9659  elznn  9660  elz2  9716  zapne  9719  3halfnz  9743  prime  9745  raluz2  9979  rexuz2  9981  supinfneg  9995  infsupneg  9996  eluz2b2  10003  eluz2b3  10004  ublbneg  10013  elq  10022  qreccl  10042  elpq  10049  ralrp  10076  rexrp  10077  rpnegap  10087  ltxr  10177  xrnemnf  10179  xrltso  10198  icc0r  10328  divelunit  10404  fzprval  10489  fztpval  10490  elfz1b  10497  fz01or  10518  4fvwrd4  10547  fzolb  10561  fzolb2  10562  elfzo3  10571  fzouzsplit  10588  elfzo0z  10596  fzo0m  10604  fzind2  10658  infssfzcldc  10669  infssfzledc  10670  ioo0  10694  ico0  10696  ioc0  10697  uzennn  10873  seq3f1olemp  10952  sseqn  11279  hashfibc  11283  hashf1lem2  11286  iswrd  11306  caucvgre  11747  cvg1nlemcau  11750  resqrexlemex  11791  climeu  12062  fsum2dlemstep  12201  expcnv  12271  prodsnf  12359  fprod2dlemstep  12389  divides  12556  m1exp1  12668  divalgb  12692  bitsval2  12711  bitsmod  12723  bitscmp  12725  bezoutlemnewy  12773  bezoutlemmain  12775  bezoutlemex  12778  dfgcd2  12791  nnwosdc  12816  lcmgcdlem  12855  isprm2  12895  isprm3  12896  isprm4  12897  isprm5  12920  sqrt2irr  12940  oddpwdc  12952  pythagtriplem19  13061  pythagtrip  13062  pceu  13074  dvdsprmpweqnn  13115  4sqlem2  13168  4sqlem12  13181  dec5dvds2  13192  ballotfilemodife  13240  ballotfilem4  13241  ennnfoneleminc  13302  ennnfonelemex  13305  ennnfonelemr  13314  ctiunct  13331  infpn2  13347  xpsfrnel  13665  xpsfrnel2  13667  gzsum0  13713  ismnd  13732  dfgrp2e  13833  dfgrp3me  13905  isnsg2  14006  eqger  14027  isabl2  14097  imasabl  14140  isrhm  14465  isrim  14476  isnzr2  14491  drngprop  14617  lss1d  14720  istps  15133  istps2  15134  isbasis2g  15146  tgval2  15152  txuni2  15357  tx1cn  15370  tx2cn  15371  uptx  15375  txdis1cn  15379  blres  15535  xmeterval  15536  xmeter  15537  isxms2  15553  isms2  15555  metrest  15607  qtopbasss  15622  dedekindicclemicc  15733  limcdifap  15763  plyrecj  15864  pilem1  15880  sincosq1lem  15926  mpodvdsmulf1o  16104  gausslemma2dlem1a  16177  gausslemma2dlem4  16183  lgsquadlem1  16196  lgsquadlem2  16197  2lgslem1b  16208  2sqlem1  16233  upgrex  16344  griedg0ssusgr  16492  clwwlkn1loopb  16661  clwwlknon2x  16676  decidr  16824  bdcuni  16902  bdcriota  16909  bdinex1  16925  bj-zfpair2  16936  bj-axun2  16941  bj-ssom  16962  ss1oel2o  17017  nninfsellemdc  17053  nninfsellemsuc  17055  nninfsellemqall  17058  trirec0xor  17094  iswomni0  17101  alsralrex  17153  alsraln0m  17154  2alsraln0m  17158  2alsraln0idm  17159  dfalseu2  17177