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  4205  dftr5  4234  trint  4246  inex1  4269  inuni  4293  repizf2lem  4300  unidif0  4306  axpweq  4310  bnd2  4312  exmid01  4337  zfpair2  4349  exss  4369  elop  4373  opm  4376  otth  4384  copsex4g  4389  opeqsn  4395  opelopabsbALT  4403  brabga  4408  opelopabaf  4418  iunopab  4426  pwunss  4430  pocl  4450  frirrg  4497  elsuci  4550  elsucg  4551  sucel  4557  unisucg  4561  uniuni  4599  reusv3  4608  iunpw  4628  setindel  4687  elirr  4690  en2lp  4703  ordpwsucss  4716  zfregfr  4723  tfi  4731  peano2  4744  peano5  4747  elxp  4793  opelxp  4806  brxp  4807  rabxp  4814  opthprc  4828  brab2a  4830  opeliunxp  4832  xpundi  4833  xpundir  4834  elvvv  4840  brinxp  4845  brab2ga  4852  0xp  4857  ssrel2  4867  eqrelrel  4878  reliun  4900  reluni  4902  raliunxp  4923  rexiunxp  4924  ralxpf  4928  rexxpf  4929  iunxpf  4930  relop  4932  elco  4948  elcnv  4959  elcnv2  4960  dmin  4991  dmuni  4993  dmopab  4994  dmi  4998  dmmrnm  5003  rnopab  5031  elrnmpt1  5035  rncoeq  5058  resiexg  5111  restidsing  5122  dfima2  5131  dfima3  5132  elima2  5135  elima3  5136  imai  5146  elimasn  5157  epini  5161  dfse2  5163  cotr  5172  issref  5173  intasym  5175  asymref  5176  cnvopab  5192  cnvi  5195  cnvdif  5197  imainss  5206  rnxpid  5225  dfrel2  5241  dfrel3  5248  dmsnm  5256  rnsnm  5257  relsn2m  5261  dmsnopg  5262  cnvcnvsn  5267  elxp4  5278  elxp5  5279  cnvresima  5280  mptpreima  5284  dfco2  5290  coundi  5292  coundir  5293  imaco  5296  coiun  5300  coi1  5306  relssdmrn  5311  relrelss  5317  unixpm  5326  ressn  5331  cnviinm  5332  cnvpom  5333  cnvsom  5334  cbviota  5345  iotass  5358  eliota  5368  dffun2  5390  dffun4  5391  dffun7  5407  dffun8  5408  dffun9  5409  funopab  5415  funun  5425  funcnvsn  5429  fntpg  5440  funcnv2  5444  funcnv  5445  fun2cnv  5448  fncnv  5450  fun11  5451  fununi  5452  imadiflem  5463  imadif  5464  imainlem  5465  funimaexglem  5467  fnunsn  5493  fnres  5503  fnopabg  5510  mptfng  5512  mptun  5518  fun  5564  fcnvres  5578  dff12  5600  f1cnvcnv  5612  funforn  5625  dff1o2  5647  dff1o5  5651  f1orn  5652  resdif  5664  ffoss  5675  f11o  5676  f1o00  5679  fo00  5680  elfv  5696  fv3  5721  nfvres  5735  eqfnfv3  5811  fneqeql  5820  unpreima  5836  respreima  5839  dffo3  5858  dffo5  5860  f1ompt  5862  ffnfvf  5870  fmptco  5877  funopdmsn  5898  ftpg  5902  fnressn  5904  idref  5965  abrexco  5968  dff13  5977  dff13f  5979  fliftel  6002  isoini  6027  eusvobj2  6074  acexmidlema  6079  acexmidlemb  6080  acexmidlemph  6081  acexmidlem2  6085  oprabid  6120  brabvv  6137  dfoprab2  6138  eqoprab2b  6149  dmoprab  6172  rnoprab  6174  eloprabga  6178  mpomptx  6182  resoprab  6187  ffnov  6195  elrnmpo  6205  ralrnmpo  6206  rexrnmpo  6207  ovid  6208  ovi3  6229  ov6g  6230  foov  6239  opabex3d  6354  opabex3  6355  abexssex  6358  oprabex3  6366  oprabrexex2  6367  fmpo  6441  xporderlem  6471  f1od2  6475  mpoxopovel  6516  brtpos2  6526  dmtpos  6531  tpostpos  6539  tpossym  6551  tposoprab  6555  dfsmo2  6562  tfrlem7  6592  tfrlem9  6594  tfr1onlemaccex  6623  tfrcllemaccex  6636  tfrcldm  6638  frecabex  6673  el1o  6714  dif1o  6715  dfer2  6812  brdifun  6838  eqerlem  6842  qsid  6878  iinerm  6885  riinerm  6886  erinxp  6887  brecop  6903  eroveu  6904  erovlem  6905  ecopovsym  6909  mapval2  6963  mapsn  6976  elixp  6991  ixpeq2  6998  ixpin  7009  ixpiinm  7010  mptelixpg  7020  ixpsnf1o  7022  domen  7039  isfi  7051  en1  7090  modom2  7113  xpsnen  7123  xpcomco  7128  xpassen  7132  ssenen  7156  nneneq  7162  snnen2oprc  7165  ac6sfi  7206  exmidpw  7219  exmidpweq  7220  pw1dc1  7225  elfpw  7266  eldju  7414  djur  7415  eldju2ndl  7418  eldju2ndr  7419  finomni  7486  nninfwlporlemd  7518  nninfwlpoimlemg  7521  acfun  7569  pw1nel3  7596  sucpw1nel3  7598  ccfunen  7636  elni  7681  ltexpi  7710  enq0enq  7804  enq0ref  7806  enq0tr  7807  prarloclem3  7870  ltdfpr  7879  genpdflem  7880  genpassl  7897  genpassu  7898  nqprrnd  7916  nqprl  7924  nqpru  7925  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemdisj  7979  ltexprlemloc  7980  recexprlemdisj  8003  caucvgprprlemell  8058  caucvgprprlemelu  8059  suplocexprlemml  8089  suplocsrlemb  8179  opelcn  8199  elreal  8201  elreal2  8203  peano1nnnn  8225  axicn  8236  axaddf  8241  axmulf  8242  axprecex  8253  axpre-ltirr  8255  axpre-mulgt0  8260  axcaucvglemres  8272  axpre-suploc  8275  xrlenlt  8396  ltxrlt  8397  inelr  8920  reapcotr  8934  1nn  9324  elnnne0  9588  un0addcl  9607  un0mulcl  9608  elnnz  9665  elznn0nn  9669  elznn0  9670  elznn  9671  elz2  9727  zapne  9730  3halfnz  9754  prime  9756  raluz2  9995  rexuz2  9997  supinfneg  10011  infsupneg  10012  eluz2b2  10019  eluz2b3  10020  ublbneg  10029  elq  10038  qreccl  10058  elpq  10066  ralrp  10093  rexrp  10094  rpnegap  10104  ltxr  10194  xrnemnf  10196  xrltso  10215  icc0r  10345  divelunit  10421  fzprval  10506  fztpval  10507  elfz1b  10514  fz01or  10535  4fvwrd4  10564  fzolb  10578  fzolb2  10579  elfzo3  10588  fzouzsplit  10605  elfzo0z  10613  fzo0m  10621  fzind2  10675  infssfzcldc  10686  infssfzledc  10687  ioo0  10711  ico0  10713  ioc0  10714  uzennn  10894  seq3f1olemp  10973  sseqn  11301  hashfibc  11305  hashf1lem2  11308  iswrd  11328  caucvgre  11769  cvg1nlemcau  11772  resqrexlemex  11813  climeu  12087  fsum2dlemstep  12226  expcnv  12296  prodsnf  12384  fprod2dlemstep  12414  divides  12581  m1exp1  12693  divalgb  12717  bitsval2  12736  bitsmod  12748  bitscmp  12750  bezoutlemnewy  12798  bezoutlemmain  12800  bezoutlemex  12803  dfgcd2  12816  nnwosdc  12841  lcmgcdlem  12880  isprm2  12920  isprm3  12921  isprm4  12922  isprm5  12946  sqrt2irr  12966  pythagtriplem19  13090  pythagtrip  13091  pceu  13103  dvdsprmpweqnn  13144  4sqlem2  13197  4sqlem12  13210  dec5dvds2  13221  ballotfilemodife  13298  ballotfilem4  13299  ennnfoneleminc  13360  ennnfonelemex  13363  ennnfonelemr  13372  ctiunct  13389  infpn2  13405  xpsfrnel  13724  xpsfrnel2  13726  gzsum0  13772  ismnd  13791  dfgrp2e  13892  dfgrp3me  13964  isnsg2  14065  eqger  14086  elcntr  14163  cntzrec  14169  isabl2  14187  imasabl  14230  idjusnfi  14270  gsum2d2fi  14274  isrhm  14574  isrim  14585  isnzr2  14600  drngprop  14726  lss1d  14829  istps  15258  istps2  15259  isbasis2g  15271  tgval2  15277  txuni2  15482  tx1cn  15495  tx2cn  15496  uptx  15500  txdis1cn  15504  blres  15660  xmeterval  15661  xmeter  15662  isxms2  15678  isms2  15680  metrest  15732  qtopbasss  15747  dedekindicclemicc  15858  limcdifap  15888  plyrecj  15989  pilem1  16006  sincosq1lem  16052  mpodvdsmulf1o  16284  gausslemma2dlem1a  16382  gausslemma2dlem4  16388  lgsquadlem1  16401  lgsquadlem2  16402  2lgslem1b  16413  2sqlem1  16438  upgrex  16549  griedg0ssusgr  16697  clwwlkn1loopb  16866  clwwlknon2x  16881  decidr  17029  bdcuni  17107  bdcriota  17114  bdinex1  17130  bj-zfpair2  17141  bj-axun2  17146  bj-ssom  17167  ss1oel2o  17222  idjudju  17252  nninfsellemdc  17259  nninfsellemsuc  17261  nninfsellemqall  17264  trirec0xor  17301  iswomni0  17308  alsralrex  17360  alsraln0m  17361  2alsraln0m  17365  2alsraln0idm  17366  dfalseu2  17384