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  7409  djur  7410  eldju2ndl  7413  eldju2ndr  7414  finomni  7481  nninfwlporlemd  7513  nninfwlpoimlemg  7516  acfun  7564  pw1nel3  7591  sucpw1nel3  7593  ccfunen  7631  elni  7676  ltexpi  7705  enq0enq  7799  enq0ref  7801  enq0tr  7802  prarloclem3  7865  ltdfpr  7874  genpdflem  7875  genpassl  7892  genpassu  7893  nqprrnd  7911  nqprl  7919  nqpru  7920  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemdisj  7974  ltexprlemloc  7975  recexprlemdisj  7998  caucvgprprlemell  8053  caucvgprprlemelu  8054  suplocexprlemml  8084  suplocsrlemb  8174  opelcn  8194  elreal  8196  elreal2  8198  peano1nnnn  8220  axicn  8231  axaddf  8236  axmulf  8237  axprecex  8248  axpre-ltirr  8250  axpre-mulgt0  8255  axcaucvglemres  8267  axpre-suploc  8270  xrlenlt  8391  ltxrlt  8392  inelr  8915  reapcotr  8929  1nn  9318  elnnne0  9582  un0addcl  9601  un0mulcl  9602  elnnz  9659  elznn0nn  9663  elznn0  9664  elznn  9665  elz2  9721  zapne  9724  3halfnz  9748  prime  9750  raluz2  9989  rexuz2  9991  supinfneg  10005  infsupneg  10006  eluz2b2  10013  eluz2b3  10014  ublbneg  10023  elq  10032  qreccl  10052  elpq  10060  ralrp  10087  rexrp  10088  rpnegap  10098  ltxr  10188  xrnemnf  10190  xrltso  10209  icc0r  10339  divelunit  10415  fzprval  10500  fztpval  10501  elfz1b  10508  fz01or  10529  4fvwrd4  10558  fzolb  10572  fzolb2  10573  elfzo3  10582  fzouzsplit  10599  elfzo0z  10607  fzo0m  10615  fzind2  10669  infssfzcldc  10680  infssfzledc  10681  ioo0  10705  ico0  10707  ioc0  10708  uzennn  10888  seq3f1olemp  10967  sseqn  11295  hashfibc  11299  hashf1lem2  11302  iswrd  11322  caucvgre  11763  cvg1nlemcau  11766  resqrexlemex  11807  climeu  12081  fsum2dlemstep  12220  expcnv  12290  prodsnf  12378  fprod2dlemstep  12408  divides  12575  m1exp1  12687  divalgb  12711  bitsval2  12730  bitsmod  12742  bitscmp  12744  bezoutlemnewy  12792  bezoutlemmain  12794  bezoutlemex  12797  dfgcd2  12810  nnwosdc  12835  lcmgcdlem  12874  isprm2  12914  isprm3  12915  isprm4  12916  isprm5  12940  sqrt2irr  12960  pythagtriplem19  13084  pythagtrip  13085  pceu  13097  dvdsprmpweqnn  13138  4sqlem2  13191  4sqlem12  13204  dec5dvds2  13215  ballotfilemodife  13292  ballotfilem4  13293  ennnfoneleminc  13354  ennnfonelemex  13357  ennnfonelemr  13366  ctiunct  13383  infpn2  13399  xpsfrnel  13718  xpsfrnel2  13720  gzsum0  13766  ismnd  13785  dfgrp2e  13886  dfgrp3me  13958  isnsg2  14059  eqger  14080  elcntr  14157  cntzrec  14163  isabl2  14181  imasabl  14224  isrhm  14549  isrim  14560  isnzr2  14575  drngprop  14701  lss1d  14804  istps  15224  istps2  15225  isbasis2g  15237  tgval2  15243  txuni2  15448  tx1cn  15461  tx2cn  15462  uptx  15466  txdis1cn  15470  blres  15626  xmeterval  15627  xmeter  15628  isxms2  15644  isms2  15646  metrest  15698  qtopbasss  15713  dedekindicclemicc  15824  limcdifap  15854  plyrecj  15955  pilem1  15972  sincosq1lem  16018  mpodvdsmulf1o  16245  gausslemma2dlem1a  16343  gausslemma2dlem4  16349  lgsquadlem1  16362  lgsquadlem2  16363  2lgslem1b  16374  2sqlem1  16399  upgrex  16510  griedg0ssusgr  16658  clwwlkn1loopb  16827  clwwlknon2x  16842  decidr  16990  bdcuni  17068  bdcriota  17075  bdinex1  17091  bj-zfpair2  17102  bj-axun2  17107  bj-ssom  17128  ss1oel2o  17183  nninfsellemdc  17219  nninfsellemsuc  17221  nninfsellemqall  17224  trirec0xor  17261  iswomni0  17268  alsralrex  17320  alsraln0m  17321  2alsraln0m  17325  2alsraln0idm  17326  dfalseu2  17344