Theorem bitri 182

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 118	. . 3 |- ( ph -> ps )
3		bitri.2	. . 3 |- ( ps <-> ch )
4	2, 3	sylib 120	. 2 |- ( ph -> ch )
5	3	biimpri 131	. . 3 |- ( ch -> ps )
6	5, 1	sylibr 132	. 2 |- ( ch -> ph )
7	4, 6	impbii 124	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bitr2i  183  bitr3i  184  bitr4i  185  bitrd  186  3bitri  204  3bitr2i  206  3bitr3i  208  3bitr4i  210  bibi12i  227  imbi12i  237  pm4.71r  382  biadan2  444  anbi2ci  447  anbi12i  448  anbi12ci  449  pm5.3  459  an42  552  xchbinx  640  mt2bi  642  orbi12i  714  or42  722  pm5.53  749  orddi  767  anddi  768  pm2.1dc  781  notnotrdc  787  dcim  820  testbitestn  859  rbaib  866  rbaibr  867  pm4.43  893  orbididc  897  pm5.75  906  3orass  925  3anass  926  3ancomb  930  3anan32  933  3anan12  934  anandi3  935  anandi3r  936  xordc  1326  falbitru  1351  19.26-2  1414  19.26-3an  1415  alrot3  1417  albiim  1419  2albiim  1420  19.27h  1495  19.27  1496  19.28h  1497  19.28  1498  nfalt  1513  aaanh  1521  aaan  1522  alinexa  1537  19.21-2  1600  nf2  1601  19.44  1615  19.45  1616  exrot3  1623  exrot4  1624  eeor  1628  sbcof2  1735  sbid2h  1774  19.23vv  1809  sbnv  1813  sblimv  1819  pm11.53  1820  19.41vv  1828  19.41vvv  1829  19.41vvvv  1830  19.42vv  1833  19.42vvv  1834  19.42vvvv  1835  4exdistr  1838  cbvex4v  1850  eean  1851  sbn  1871  sbim  1872  sbor  1873  sban  1874  sbrim  1875  sblim  1876  sbbi  1878  sblbis  1879  sbrbis  1880  sbrbif  1881  sbco2d  1885  sbco2vd  1886  sbnf2  1902  2sb5  1904  2sb6  1905  sbcom2v  1906  sbcom2v2  1907  sbcom2  1908  sb6a  1909  2sb5rf  1910  2sb6rf  1911  sbalyz  1920  sbal  1921  sbal1yz  1922  sbex  1925  sbalv  1926  sbco4lem  1927  exsb  1929  2exsb  1930  eujust  1947  euf  1950  cbveu  1969  mor  1987  eu2  1989  mo4f  2005  eu4  2007  2exeu  2037  2eu4  2038  exists1  2041  abid  2073  eleq12i  2152  abeq2  2193  abeq2i  2195  clabel  2210  abid2f  2249  sbabel  2250  neeq12i  2268  neanior  2338  ralnex  2365  dfrex2dc  2367  ralinexa  2401  nfraldya  2408  nfrexdya  2409  r3al  2416  r19.26-2  2494  ralbiim  2499  r19.43  2521  ralcomf  2524  rexcomf  2525  rexrot4  2529  reean  2531  3reeanv  2533  rabbi  2540  cbvralf  2580  cbvrexf  2581  cbvreu  2584  cbvral2v  2594  cbvrex2v  2595  cbvral3v  2596  cbvralsv  2597  cbvrexsv  2598  sbralie  2599  rabeq2i  2612  issetf  2620  2gencl  2646  3gencl  2647  ceqsex2  2653  ceqsex3v  2655  ceqsex6v  2657  ceqsex8v  2658  gencbvex  2659  gencbval  2661  spc2gv  2702  eqvincf  2733  ceqsrex2v  2740  elrab2  2765  ralab  2766  ralrab  2767  rexab  2768  rexrab  2769  ralab2  2770  rexab2  2772  eueq3dc  2780  morex  2790  euind  2793  reu2  2794  reu6  2795  rmo4  2799  reu4  2800  reu7  2801  rmoim  2805  2reuswapdc  2808  reuind  2809  2rmorex  2810  sbcco  2850  sbccomlem  2902  sbccom  2903  ra5  2916  rmo3  2919  csbco  2931  sbnfc2  2977  csbabg  2978  cbvralcsf  2979  cbvrexcsf  2980  cbvreucsf  2981  dfss  3002  dfss2f  3005  ss2ab  3078  dfdif3  3099  difeqri  3109  ddifstab  3121  raldifb  3129  uneqri  3131  ssequn2  3162  unss  3163  rexun  3169  ralunb  3170  elin2  3177  ineqri  3182  dfss1  3193  dfss5  3194  dfss4st  3221  ssddif  3222  difin  3225  indif  3231  difundi  3240  indifdir  3244  symdifxor  3254  inrab2  3261  rabun2  3267  reuun2  3271  0el  3294  rabeq0  3301  abeq0  3302  disjr  3320  disj1  3321  undif4  3333  uneqdifeqim  3355  r19.3rm  3357  r19.9rmv  3360  raaan  3375  pwss  3430  dfpr2  3450  ralsnsg  3463  ralsns  3464  eltpg  3471  ralprg  3476  rexprg  3477  raltpg  3478  rextpg  3479  snprc  3490  rabrsndc  3493  euabsn2  3494  eusn  3499  eldifsn  3550  ssdifsn  3551  rexdifsn  3555  eqsnm  3582  tpss  3585  snsssn  3588  prel12  3598  preqsn  3602  oprcl  3629  pwtpss  3633  eluniab  3648  elunirab  3649  unipr  3650  dfnfc2  3654  uniun  3655  uniin  3656  uni0b  3661  unissb  3666  elintab  3682  elintrab  3683  ssintab  3688  ssintrab  3694  intun  3702  intpr  3703  elrint  3711  iuncom4  3720  iuneq2  3729  dfiun2g  3745  ssiinf  3762  iundif2ss  3778  elriin  3783  iunxiun  3792  pwssb  3796  iunpwss  3799  dfdisj2  3803  cbvopab1  3886  dftr5  3914  trint  3926  inex1  3948  inuni  3966  repizf2lem  3971  unidif0  3977  axpweq  3981  bnd2  3983  exmid01  4006  zfpair2  4011  exss  4028  elop  4032  opm  4035  otth  4043  copsex4g  4048  opeqsn  4053  opelopabsbALT  4060  brabga  4065  opelopabaf  4074  iunopab  4082  pwunss  4084  pocl  4104  frirrg  4151  elsuci  4204  elsucg  4205  sucel  4211  unisucg  4215  uniuni  4247  reusv3  4256  iunpw  4275  setindel  4327  elirr  4330  en2lp  4343  ordpwsucss  4356  zfregfr  4362  tfi  4370  peano2  4383  peano5  4386  elxp  4428  opelxp  4440  brxp  4441  rabxp  4446  opthprc  4457  brab2a  4459  opeliunxp  4461  xpundi  4462  xpundir  4463  elvvv  4469  brinxp  4474  brab2ga  4481  0xp  4486  ssrel2  4496  eqrelrel  4507  reliun  4526  reluni  4528  raliunxp  4545  rexiunxp  4546  ralxpf  4550  rexxpf  4551  iunxpf  4552  relop  4554  elco  4570  elcnv  4581  elcnv2  4582  dmin  4612  dmuni  4614  dmopab  4615  dmi  4619  dmmrnm  4623  rnopab  4650  elrnmpt1  4654  rncoeq  4674  resiexg  4724  dfima2  4743  dfima3  4744  elima2  4747  elima3  4748  imai  4755  elimasn  4766  epini  4770  dfse2  4772  cotr  4780  issref  4781  intasym  4783  asymref  4784  cnvopab  4800  cnvi  4802  cnvdif  4804  imainss  4813  rnxpid  4831  dfrel2  4847  dfrel3  4854  dmsnm  4862  rnsnm  4863  relsn2m  4867  dmsnopg  4868  cnvcnvsn  4873  elxp4  4884  elxp5  4885  cnvresima  4886  mptpreima  4890  dfco2  4896  coundi  4898  coundir  4899  imaco  4902  coiun  4906  coi1  4912  relssdmrn  4917  relrelss  4923  unixpm  4932  ressn  4937  cnviinm  4938  cnvpom  4939  cnvsom  4940  cbviota  4951  iotass  4963  dffun2  4991  dffun4  4992  dffun7  5007  dffun8  5008  dffun9  5009  funopab  5014  funun  5023  funcnvsn  5024  fntpg  5035  funcnv2  5039  funcnv  5040  fun2cnv  5043  fncnv  5045  fun11  5046  fununi  5047  imadiflem  5058  imadif  5059  imainlem  5060  funimaexglem  5062  fnunsn  5086  fnres  5095  fnopabg  5102  mptfng  5104  mptun  5109  fun  5147  fcnvres  5157  dff12  5178  f1cnvcnv  5190  funforn  5203  dff1o2  5221  dff1o5  5225  f1orn  5226  resdif  5238  ffoss  5248  f11o  5249  f1o00  5251  fo00  5252  elfv  5266  fv3  5291  nfvres  5300  eqfnfv3  5362  fneqeql  5370  unpreima  5387  respreima  5390  dffo3  5409  dffo5  5411  f1ompt  5413  ffnfvf  5420  fmptco  5427  ftpg  5444  fnressn  5446  idref  5497  abrexco  5499  dff13  5508  dff13f  5510  fliftel  5533  isoini  5558  eusvobj2  5599  acexmidlema  5604  acexmidlemb  5605  acexmidlemph  5606  acexmidlem2  5610  oprabid  5638  brabvv  5652  dfoprab2  5653  eqoprab2b  5664  dmoprab  5686  rnoprab  5688  eloprabga  5692  mpt2mptx  5696  resoprab  5698  ffnov  5706  elrnmpt2  5715  ralrnmpt2  5716  rexrnmpt2  5717  ovid  5718  ovi3  5738  ov6g  5739  foov  5748  opabex3d  5849  opabex3  5850  abexssex  5853  oprabex3  5857  oprabrexex2  5858  fmpt2  5928  xporderlem  5953  f1od2  5957  mpt2xopovel  5960  brtpos2  5970  dmtpos  5975  tpostpos  5983  tpossym  5995  tposoprab  5999  dfsmo2  6006  tfrlem7  6036  tfrlem9  6038  tfr1onlemaccex  6067  tfrcllemaccex  6080  tfrcldm  6082  frecabex  6117  el1o  6155  dif1o  6156  dfer2  6245  brdifun  6271  eqerlem  6275  qsid  6309  iinerm  6316  riinerm  6317  erinxp  6318  brecop  6334  eroveu  6335  erovlem  6336  ecopovsym  6340  mapval2  6387  mapsn  6399  domen  6420  isfi  6430  en1  6468  xpsnen  6489  xpcomco  6494  xpassen  6498  ssenen  6519  nneneq  6525  snnen2oprc  6528  ac6sfi  6566  exmidpw  6576  eldju  6703  eldju2ndl  6707  eldju2ndr  6708  finomni  6740  elni  6811  ltexpi  6840  enq0enq  6934  enq0ref  6936  enq0tr  6937  prarloclem3  7000  ltdfpr  7009  genpdflem  7010  genpassl  7027  genpassu  7028  nqprrnd  7046  nqprl  7054  nqpru  7055  ltexprlemopl  7104  ltexprlemopu  7106  ltexprlemdisj  7109  ltexprlemloc  7110  recexprlemdisj  7133  caucvgprprlemell  7188  caucvgprprlemelu  7189  opelcn  7308  elreal  7310  elreal2  7312  peano1nnnn  7333  axicn  7344  axprecex  7359  axpre-ltirr  7361  axpre-mulgt0  7366  axcaucvglemres  7378  xrlenlt  7495  ltxrlt  7496  inelr  8002  reapcotr  8016  1nn  8368  elnnne0  8620  un0addcl  8639  un0mulcl  8640  elnnz  8693  elznn0nn  8697  elznn0  8698  elznn  8699  elz2  8751  zapne  8754  3halfnz  8776  prime  8778  raluz2  8999  rexuz2  9001  supinfneg  9015  infsupneg  9016  eluz2b2  9022  eluz2b3  9023  ublbneg  9030  elq  9039  qreccl  9059  ralrp  9087  rexrp  9088  rpnegap  9098  ltxr  9178  xrnemnf  9180  xrltso  9198  icc0r  9276  divelunit  9351  fzprval  9426  fztpval  9427  elfz1b  9434  fz01or  9455  4fvwrd4  9479  fzolb  9492  fzolb2  9493  elfzo3  9502  fzouzsplit  9518  elfzo0z  9523  fzo0m  9530  fzind2  9578  ioo0  9599  ico0  9601  ioc0  9602  iseqf1olemp  9835  caucvgre  10309  cvg1nlemcau  10312  resqrexlemex  10353  climeu  10577  divides  10673  m1exp1  10776  divalgb  10800  bezoutlemnewy  10860  bezoutlemmain  10862  bezoutlemex  10865  dfgcd2  10878  lcmgcdlem  10934  isprm2  10974  isprm3  10975  isprm4  10976  sqrt2irr  11016  oddpwdc  11027  decidr  11134  bdcuni  11205  bdcriota  11212  bdinex1  11228  bj-zfpair2  11239  bj-axun2  11244  bj-ssom  11269  ss1oel2o  11326  nninfsellemdc  11340  nninfsellemsuc  11342  nninfsellemqall  11345