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  390  biadan2  456  anbi2ci  459  anbi12i  460  anbi12ci  461  bianassc  470  pm5.3  475  an42  589  xchbinx  689  mt2bi  691  orbi12i  772  or42  780  pm5.53  810  orddi  828  anddi  829  pm2.1dc  845  dcim  849  notnotrdc  851  dcnnOLD  857  rbaib  929  rbaibr  930  pm4.43  958  orbididc  962  pm5.75  971  ifptru  998  ifpfal  999  3orass  1008  3anass  1009  3ancomb  1013  3anan32  1016  3anan12  1017  anandi3  1018  anandi3r  1019  xordc  1437  falbitru  1462  19.26-2  1531  19.26-3an  1532  alrot3  1534  albiim  1536  2albiim  1537  19.27h  1609  19.27  1610  19.28h  1611  19.28  1612  nfalt  1627  aaanh  1635  aaan  1636  alinexa  1652  19.21-2  1715  nf2  1716  19.44  1730  19.45  1731  exrot3  1738  exrot4  1739  eeor  1743  sbcof2  1859  sbid2h  1898  19.23vv  1933  sbnv  1939  sblimv  1946  pm11.53  1947  19.41vv  1955  19.41vvv  1956  19.41vvvv  1957  exdistrv  1962  19.42vv  1963  19.42vvv  1964  19.42vvvv  1965  4exdistr  1968  cbvex4v  1986  eean  1987  sbn  2008  sbim  2009  sbor  2010  sban  2011  sbrim  2012  sblim  2013  sbbi  2015  sblbis  2016  sbrbis  2017  sbrbif  2018  sbco2d  2022  sbco2vd  2023  sbnf2  2037  2sb5  2039  2sb6  2040  sbcom2v  2041  sbcom2v2  2042  sbcom2  2043  sb6a  2044  2sb5rf  2045  2sb6rf  2046  sbalyz  2055  sbal  2056  sbal1yz  2057  sbex  2060  sbalv  2061  sbco4lem  2062  exsb  2064  2exsb  2065  eujust  2084  euf  2087  cbveu  2106  mor  2125  eu2  2127  mo4f  2143  eu4  2145  2exeu  2175  2eu4  2176  exists1  2179  abid  2222  eleq12i  2302  abeq2  2343  abeq2i  2345  abbib  2352  clabel  2363  eqabb  2370  abid2f  2412  sbabel  2413  neeq12i  2431  neanior  2501  ralnex  2532  dfrex2dc  2535  ralinexa  2571  nfraldya  2579  nfrexdya  2580  r3al  2588  r19.26-2  2674  ralbiim  2679  ralnex2  2684  r19.43  2703  ralcomf  2706  rexcomf  2707  ralrot3  2710  rexrot4  2712  reean  2714  3reeanv  2716  reqabi  2722  rabbi  2724  cbvralf  2771  cbvrexf  2772  cbvreu  2778  cbvral2vw  2791  cbvrex2vw  2792  cbvral2v  2793  cbvrex2v  2794  cbvral3v  2795  cbvralsv  2796  cbvrexsv  2797  sbralie  2798  rabeq2i  2812  issetf  2823  2gencl  2849  3gencl  2850  ceqsex2  2857  ceqsex3v  2859  ceqsex6v  2861  ceqsex8v  2862  gencbvex  2863  gencbval  2865  spc2gv  2910  eqvincf  2944  ceqsrex2v  2951  clel5  2956  elrab2  2978  ralab  2979  ralrab  2980  rexab  2981  rexrab  2982  ralab2  2983  rexab2  2985  eueq3dc  2993  morex  3003  euind  3006  reu2  3007  reu6  3008  rmo4  3012  reu4  3013  reu7  3014  rmo3f  3016  rmo4f  3017  rmoim  3020  2reuswapdc  3023  reuind  3024  2rmorex  3025  sbcco  3066  sbccomlem  3119  sbccom  3120  ra5  3134  rmo3  3137  csbco  3150  csbcow  3151  sbnfc2  3201  csbabg  3202  cbvralcsf  3203  cbvrexcsf  3204  cbvreucsf  3205  dfss  3227  dfss2f  3231  ss2ab  3308  dfdif3  3331  difeqri  3341  ddifstab  3353  raldifb  3361  uneqri  3363  ssequn2  3394  unss  3395  rexun  3401  ralunb  3402  elin2  3409  ineqri  3416  dfss1  3427  dfss5  3428  dfss4st  3456  ssddif  3457  difin  3460  indif  3466  difundi  3475  indifdir  3479  symdifxor  3489  inrab2  3496  rabun2  3502  reuun2  3506  0el  3533  rabeq0  3540  abeq0  3541  disjr  3560  disj1  3561  undif4  3573  uneqdifeqim  3597  r19.2m  3598  r19.3rm  3600  r19.9rmv  3603  raaan  3617  pwss  3690  dfpr2  3710  rexdifpr  3719  ralsnsg  3728  ralsns  3729  eltpg  3736  eldiftp  3737  ralprg  3742  rexprg  3743  raltpg  3744  rextpg  3745  snprc  3756  rabrsndc  3761  euabsn2  3762  eusn  3767  eldifsn  3822  ssdifsn  3823  rexdifsn  3827  eqsnm  3861  tpss  3864  snsssn  3867  prel12  3877  preqsn  3881  oprcl  3909  pwtpss  3913  eluniab  3928  elunirab  3929  unipr  3930  dfnfc2  3934  uniun  3935  uniin  3936  uni0b  3941  unissb  3946  elintab  3962  elintrab  3963  ssintab  3968  ssintrab  3974  intun  3982  intpr  3983  elrint  3991  iuncom4  4000  iuneq2  4009  dfiun2g  4025  ssiinf  4043  iundif2ss  4059  elriin  4064  iunxiun  4075  pwssb  4079  elpwpw  4080  iunpwss  4085  dfdisj2  4089  disjiun  4106  cbvopab1  4185  dftr5  4213  trint  4225  inex1  4246  inuni  4269  repizf2lem  4276  unidif0  4282  axpweq  4286  bnd2  4288  exmid01  4313  zfpair2  4325  exss  4345  elop  4349  opm  4352  otth  4360  copsex4g  4365  opeqsn  4371  opelopabsbALT  4379  brabga  4384  opelopabaf  4394  iunopab  4402  pwunss  4406  pocl  4426  frirrg  4473  elsuci  4526  elsucg  4527  sucel  4533  unisucg  4537  uniuni  4574  reusv3  4583  iunpw  4603  setindel  4662  elirr  4665  en2lp  4678  ordpwsucss  4691  zfregfr  4698  tfi  4706  peano2  4719  peano5  4722  elxp  4768  opelxp  4781  brxp  4782  rabxp  4789  opthprc  4803  brab2a  4805  opeliunxp  4807  xpundi  4808  xpundir  4809  elvvv  4815  brinxp  4820  brab2ga  4827  0xp  4832  ssrel2  4842  eqrelrel  4853  reliun  4875  reluni  4877  raliunxp  4898  rexiunxp  4899  ralxpf  4903  rexxpf  4904  iunxpf  4905  relop  4907  elco  4923  elcnv  4934  elcnv2  4935  dmin  4966  dmuni  4968  dmopab  4969  dmi  4973  dmmrnm  4978  rnopab  5006  elrnmpt1  5010  rncoeq  5033  resiexg  5085  restidsing  5096  dfima2  5105  dfima3  5106  elima2  5109  elima3  5110  imai  5120  elimasn  5131  epini  5135  dfse2  5137  cotr  5146  issref  5147  intasym  5149  asymref  5150  cnvopab  5166  cnvi  5169  cnvdif  5171  imainss  5180  rnxpid  5199  dfrel2  5215  dfrel3  5222  dmsnm  5230  rnsnm  5231  relsn2m  5235  dmsnopg  5236  cnvcnvsn  5241  elxp4  5252  elxp5  5253  cnvresima  5254  mptpreima  5258  dfco2  5264  coundi  5266  coundir  5267  imaco  5270  coiun  5274  coi1  5280  relssdmrn  5285  relrelss  5291  unixpm  5300  ressn  5305  cnviinm  5306  cnvpom  5307  cnvsom  5308  cbviota  5319  iotass  5332  eliota  5342  dffun2  5364  dffun4  5365  dffun7  5381  dffun8  5382  dffun9  5383  funopab  5389  funun  5399  funcnvsn  5403  fntpg  5414  funcnv2  5418  funcnv  5419  fun2cnv  5422  fncnv  5424  fun11  5425  fununi  5426  imadiflem  5437  imadif  5438  imainlem  5439  funimaexglem  5441  fnunsn  5467  fnres  5477  fnopabg  5484  mptfng  5486  mptun  5492  fun  5538  fcnvres  5552  dff12  5574  f1cnvcnv  5586  funforn  5599  dff1o2  5621  dff1o5  5625  f1orn  5626  resdif  5638  ffoss  5649  f11o  5650  f1o00  5653  fo00  5654  elfv  5670  fv3  5695  nfvres  5708  eqfnfv3  5779  fneqeql  5788  unpreima  5804  respreima  5807  dffo3  5826  dffo5  5828  f1ompt  5830  ffnfvf  5838  fmptco  5845  funopdmsn  5866  ftpg  5870  fnressn  5872  idref  5931  abrexco  5934  dff13  5943  dff13f  5945  fliftel  5968  isoini  5993  eusvobj2  6038  acexmidlema  6043  acexmidlemb  6044  acexmidlemph  6045  acexmidlem2  6049  oprabid  6084  brabvv  6101  dfoprab2  6102  eqoprab2b  6113  dmoprab  6136  rnoprab  6138  eloprabga  6142  mpomptx  6146  resoprab  6151  ffnov  6159  elrnmpo  6169  ralrnmpo  6170  rexrnmpo  6171  ovid  6172  ovi3  6193  ov6g  6194  foov  6203  opabex3d  6316  opabex3  6317  abexssex  6320  oprabex3  6324  oprabrexex2  6325  fmpo  6399  xporderlem  6429  f1od2  6433  mpoxopovel  6474  brtpos2  6484  dmtpos  6489  tpostpos  6497  tpossym  6509  tposoprab  6513  dfsmo2  6520  tfrlem7  6550  tfrlem9  6552  tfr1onlemaccex  6581  tfrcllemaccex  6594  tfrcldm  6596  frecabex  6631  el1o  6672  dif1o  6673  dfer2  6770  brdifun  6796  eqerlem  6800  qsid  6836  iinerm  6843  riinerm  6844  erinxp  6845  brecop  6861  eroveu  6862  erovlem  6863  ecopovsym  6867  mapval2  6914  mapsn  6927  elixp  6942  ixpeq2  6949  ixpin  6960  ixpiinm  6961  mptelixpg  6971  ixpsnf1o  6973  domen  6990  isfi  7002  en1  7041  modom2  7064  xpsnen  7074  xpcomco  7079  xpassen  7083  ssenen  7107  nneneq  7113  snnen2oprc  7116  ac6sfi  7157  exmidpw  7170  exmidpweq  7171  pw1dc1  7176  elfpw  7217  eldju  7361  djur  7362  eldju2ndl  7365  eldju2ndr  7366  finomni  7433  nninfwlporlemd  7465  nninfwlpoimlemg  7468  acfun  7516  pw1nel3  7543  sucpw1nel3  7545  ccfunen  7580  elni  7625  ltexpi  7654  enq0enq  7748  enq0ref  7750  enq0tr  7751  prarloclem3  7814  ltdfpr  7823  genpdflem  7824  genpassl  7841  genpassu  7842  nqprrnd  7860  nqprl  7868  nqpru  7869  ltexprlemopl  7918  ltexprlemopu  7920  ltexprlemdisj  7923  ltexprlemloc  7924  recexprlemdisj  7947  caucvgprprlemell  8002  caucvgprprlemelu  8003  suplocexprlemml  8033  suplocsrlemb  8123  opelcn  8143  elreal  8145  elreal2  8147  peano1nnnn  8169  axicn  8180  axaddf  8185  axmulf  8186  axprecex  8197  axpre-ltirr  8199  axpre-mulgt0  8204  axcaucvglemres  8216  axpre-suploc  8219  xrlenlt  8340  ltxrlt  8341  inelr  8860  reapcotr  8874  1nn  9250  elnnne0  9512  un0addcl  9531  un0mulcl  9532  elnnz  9589  elznn0nn  9593  elznn0  9594  elznn  9595  elz2  9651  zapne  9654  3halfnz  9678  prime  9680  raluz2  9914  rexuz2  9916  supinfneg  9930  infsupneg  9931  eluz2b2  9938  eluz2b3  9939  ublbneg  9948  elq  9957  qreccl  9977  elpq  9984  ralrp  10011  rexrp  10012  rpnegap  10022  ltxr  10111  xrnemnf  10113  xrltso  10132  icc0r  10262  divelunit  10338  fzprval  10420  fztpval  10421  elfz1b  10428  fz01or  10449  4fvwrd4  10478  fzolb  10492  fzolb2  10493  elfzo3  10502  fzouzsplit  10519  elfzo0z  10527  fzo0m  10535  fzind2  10589  ioo0  10623  ico0  10625  ioc0  10626  uzennn  10802  seq3f1olemp  10881  sseqn  11207  hashfibc  11211  iswrd  11230  caucvgre  11670  cvg1nlemcau  11673  resqrexlemex  11714  climeu  11985  fsum2dlemstep  12124  expcnv  12194  prodsnf  12282  fprod2dlemstep  12312  divides  12479  m1exp1  12591  divalgb  12615  bitsval2  12634  bitsmod  12646  bitscmp  12648  bezoutlemnewy  12696  bezoutlemmain  12698  bezoutlemex  12701  dfgcd2  12714  nnwosdc  12739  lcmgcdlem  12778  isprm2  12818  isprm3  12819  isprm4  12820  isprm5  12843  sqrt2irr  12863  oddpwdc  12875  pythagtriplem19  12984  pythagtrip  12985  pceu  12997  dvdsprmpweqnn  13038  4sqlem2  13091  4sqlem12  13104  dec5dvds2  13115  ballotfilemodife  13158  ballotfilem4  13159  ennnfoneleminc  13179  ennnfonelemex  13182  ennnfonelemr  13191  ctiunct  13208  infpn2  13224  xpsfrnel  13574  xpsfrnel2  13576  gsum0g  13626  ismnd  13649  dfgrp2e  13758  dfgrp3me  13830  isnsg2  13937  eqger  13958  isabl2  14028  imasabl  14070  isrhm  14320  isrim  14331  isnzr2  14346  lss1d  14548  istps  14914  istps2  14915  isbasis2g  14927  tgval2  14933  txuni2  15138  tx1cn  15151  tx2cn  15152  uptx  15156  txdis1cn  15160  blres  15316  xmeterval  15317  xmeter  15318  isxms2  15334  isms2  15336  metrest  15388  qtopbasss  15403  dedekindicclemicc  15514  limcdifap  15544  plyrecj  15645  pilem1  15661  sincosq1lem  15707  mpodvdsmulf1o  15875  gausslemma2dlem1a  15948  gausslemma2dlem4  15954  lgsquadlem1  15967  lgsquadlem2  15968  2lgslem1b  15979  2sqlem1  16004  upgrex  16115  griedg0ssusgr  16263  clwwlkn1loopb  16432  clwwlknon2x  16447  decidr  16585  bdcuni  16663  bdcriota  16670  bdinex1  16686  bj-zfpair2  16697  bj-axun2  16702  bj-ssom  16723  ss1oel2o  16778  nninfsellemdc  16805  nninfsellemsuc  16807  nninfsellemqall  16810  trirec0xor  16846  iswomni0  16853