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  587  xchbinx  683  mt2bi  685  orbi12i  765  or42  773  pm5.53  803  orddi  821  anddi  822  pm2.1dc  838  dcim  842  notnotrdc  844  dcnnOLD  850  rbaib  922  rbaibr  923  pm4.43  951  orbididc  955  pm5.75  964  3orass  983  3anass  984  3ancomb  988  3anan32  991  3anan12  992  anandi3  993  anandi3r  994  xordc  1411  falbitru  1436  19.26-2  1504  19.26-3an  1505  alrot3  1507  albiim  1509  2albiim  1510  19.27h  1582  19.27  1583  19.28h  1584  19.28  1585  nfalt  1600  aaanh  1608  aaan  1609  alinexa  1625  19.21-2  1689  nf2  1690  19.44  1704  19.45  1705  exrot3  1712  exrot4  1713  eeor  1717  sbcof2  1832  sbid2h  1871  19.23vv  1906  sbnv  1911  sblimv  1917  pm11.53  1918  19.41vv  1926  19.41vvv  1927  19.41vvvv  1928  exdistrv  1933  19.42vv  1934  19.42vvv  1935  19.42vvvv  1936  4exdistr  1939  cbvex4v  1957  eean  1958  sbn  1979  sbim  1980  sbor  1981  sban  1982  sbrim  1983  sblim  1984  sbbi  1986  sblbis  1987  sbrbis  1988  sbrbif  1989  sbco2d  1993  sbco2vd  1994  sbnf2  2008  2sb5  2010  2sb6  2011  sbcom2v  2012  sbcom2v2  2013  sbcom2  2014  sb6a  2015  2sb5rf  2016  2sb6rf  2017  sbalyz  2026  sbal  2027  sbal1yz  2028  sbex  2031  sbalv  2032  sbco4lem  2033  exsb  2035  2exsb  2036  eujust  2055  euf  2058  cbveu  2077  mor  2095  eu2  2097  mo4f  2113  eu4  2115  2exeu  2145  2eu4  2146  exists1  2149  abid  2192  eleq12i  2272  abeq2  2313  abeq2i  2315  clabel  2331  abid2f  2373  sbabel  2374  neeq12i  2392  neanior  2462  ralnex  2493  dfrex2dc  2496  ralinexa  2532  nfraldya  2540  nfrexdya  2541  r3al  2549  r19.26-2  2634  ralbiim  2639  ralnex2  2644  r19.43  2663  ralcomf  2666  rexcomf  2667  ralrot3  2670  rexrot4  2672  reean  2674  3reeanv  2676  rabbi  2683  cbvralf  2729  cbvrexf  2730  cbvreu  2735  cbvral2vw  2748  cbvrex2vw  2749  cbvral2v  2750  cbvrex2v  2751  cbvral3v  2752  cbvralsv  2753  cbvrexsv  2754  sbralie  2755  rabeq2i  2768  issetf  2778  2gencl  2804  3gencl  2805  ceqsex2  2812  ceqsex3v  2814  ceqsex6v  2816  ceqsex8v  2817  gencbvex  2818  gencbval  2820  spc2gv  2863  eqvincf  2897  ceqsrex2v  2904  clel5  2909  elrab2  2931  ralab  2932  ralrab  2933  rexab  2934  rexrab  2935  ralab2  2936  rexab2  2938  eueq3dc  2946  morex  2956  euind  2959  reu2  2960  reu6  2961  rmo4  2965  reu4  2966  reu7  2967  rmo3f  2969  rmo4f  2970  rmoim  2973  2reuswapdc  2976  reuind  2977  2rmorex  2978  sbcco  3019  sbccomlem  3072  sbccom  3073  ra5  3086  rmo3  3089  csbco  3102  csbcow  3103  sbnfc2  3153  csbabg  3154  cbvralcsf  3155  cbvrexcsf  3156  cbvreucsf  3157  dfss  3179  dfss2f  3183  ss2ab  3260  dfdif3  3282  difeqri  3292  ddifstab  3304  raldifb  3312  uneqri  3314  ssequn2  3345  unss  3346  rexun  3352  ralunb  3353  elin2  3360  ineqri  3365  dfss1  3376  dfss5  3377  dfss4st  3405  ssddif  3406  difin  3409  indif  3415  difundi  3424  indifdir  3428  symdifxor  3438  inrab2  3445  rabun2  3451  reuun2  3455  0el  3482  rabeq0  3489  abeq0  3490  disjr  3509  disj1  3510  undif4  3522  uneqdifeqim  3545  r19.2m  3546  r19.3rm  3548  r19.9rmv  3551  raaan  3565  pwss  3631  dfpr2  3651  rexdifpr  3660  ralsnsg  3669  ralsns  3670  eltpg  3677  eldiftp  3678  ralprg  3683  rexprg  3684  raltpg  3685  rextpg  3686  snprc  3697  rabrsndc  3700  euabsn2  3701  eusn  3706  eldifsn  3759  ssdifsn  3760  rexdifsn  3764  eqsnm  3795  tpss  3798  snsssn  3801  prel12  3811  preqsn  3815  oprcl  3842  pwtpss  3846  eluniab  3861  elunirab  3862  unipr  3863  dfnfc2  3867  uniun  3868  uniin  3869  uni0b  3874  unissb  3879  elintab  3895  elintrab  3896  ssintab  3901  ssintrab  3907  intun  3915  intpr  3916  elrint  3924  iuncom4  3933  iuneq2  3942  dfiun2g  3958  ssiinf  3976  iundif2ss  3992  elriin  3997  iunxiun  4008  pwssb  4012  elpwpw  4013  iunpwss  4018  dfdisj2  4022  disjiun  4038  cbvopab1  4116  dftr5  4144  trint  4156  inex1  4177  inuni  4198  repizf2lem  4204  unidif0  4210  axpweq  4214  bnd2  4216  exmid01  4241  zfpair2  4253  exss  4270  elop  4274  opm  4277  otth  4285  copsex4g  4290  opeqsn  4296  opelopabsbALT  4304  brabga  4309  opelopabaf  4319  iunopab  4327  pwunss  4329  pocl  4349  frirrg  4396  elsuci  4449  elsucg  4450  sucel  4456  unisucg  4460  uniuni  4497  reusv3  4506  iunpw  4526  setindel  4585  elirr  4588  en2lp  4601  ordpwsucss  4614  zfregfr  4621  tfi  4629  peano2  4642  peano5  4645  elxp  4691  opelxp  4704  brxp  4705  rabxp  4711  opthprc  4725  brab2a  4727  opeliunxp  4729  xpundi  4730  xpundir  4731  elvvv  4737  brinxp  4742  brab2ga  4749  0xp  4754  ssrel2  4764  eqrelrel  4775  reliun  4795  reluni  4797  raliunxp  4818  rexiunxp  4819  ralxpf  4823  rexxpf  4824  iunxpf  4825  relop  4827  elco  4843  elcnv  4854  elcnv2  4855  dmin  4885  dmuni  4887  dmopab  4888  dmi  4892  dmmrnm  4896  rnopab  4924  elrnmpt1  4928  rncoeq  4951  resiexg  5003  restidsing  5014  dfima2  5023  dfima3  5024  elima2  5027  elima3  5028  imai  5037  elimasn  5048  epini  5052  dfse2  5054  cotr  5063  issref  5064  intasym  5066  asymref  5067  cnvopab  5083  cnvi  5086  cnvdif  5088  imainss  5097  rnxpid  5116  dfrel2  5132  dfrel3  5139  dmsnm  5147  rnsnm  5148  relsn2m  5152  dmsnopg  5153  cnvcnvsn  5158  elxp4  5169  elxp5  5170  cnvresima  5171  mptpreima  5175  dfco2  5181  coundi  5183  coundir  5184  imaco  5187  coiun  5191  coi1  5197  relssdmrn  5202  relrelss  5208  unixpm  5217  ressn  5222  cnviinm  5223  cnvpom  5224  cnvsom  5225  cbviota  5236  iotass  5248  eliota  5258  dffun2  5280  dffun4  5281  dffun7  5297  dffun8  5298  dffun9  5299  funopab  5305  funun  5314  funcnvsn  5318  fntpg  5329  funcnv2  5333  funcnv  5334  fun2cnv  5337  fncnv  5339  fun11  5340  fununi  5341  imadiflem  5352  imadif  5353  imainlem  5354  funimaexglem  5356  fnunsn  5382  fnres  5391  fnopabg  5398  mptfng  5400  mptun  5406  fun  5447  fcnvres  5458  dff12  5479  f1cnvcnv  5491  funforn  5504  dff1o2  5526  dff1o5  5530  f1orn  5531  resdif  5543  ffoss  5553  f11o  5554  f1o00  5556  fo00  5557  elfv  5573  fv3  5598  nfvres  5609  eqfnfv3  5678  fneqeql  5687  unpreima  5704  respreima  5707  dffo3  5726  dffo5  5728  f1ompt  5730  ffnfvf  5738  fmptco  5745  funopdmsn  5763  ftpg  5767  fnressn  5769  idref  5824  abrexco  5827  dff13  5836  dff13f  5838  fliftel  5861  isoini  5886  eusvobj2  5929  acexmidlema  5934  acexmidlemb  5935  acexmidlemph  5936  acexmidlem2  5940  oprabid  5975  brabvv  5990  dfoprab2  5991  eqoprab2b  6002  dmoprab  6025  rnoprab  6027  eloprabga  6031  mpomptx  6035  resoprab  6040  ffnov  6048  elrnmpo  6058  ralrnmpo  6059  rexrnmpo  6060  ovid  6061  ovi3  6082  ov6g  6083  foov  6092  opabex3d  6205  opabex3  6206  abexssex  6209  oprabex3  6213  oprabrexex2  6214  fmpo  6286  xporderlem  6316  f1od2  6320  mpoxopovel  6326  brtpos2  6336  dmtpos  6341  tpostpos  6349  tpossym  6361  tposoprab  6365  dfsmo2  6372  tfrlem7  6402  tfrlem9  6404  tfr1onlemaccex  6433  tfrcllemaccex  6446  tfrcldm  6448  frecabex  6483  el1o  6522  dif1o  6523  dfer2  6620  brdifun  6646  eqerlem  6650  qsid  6686  iinerm  6693  riinerm  6694  erinxp  6695  brecop  6711  eroveu  6712  erovlem  6713  ecopovsym  6717  mapval2  6764  mapsn  6776  elixp  6791  ixpeq2  6798  ixpin  6809  ixpiinm  6810  mptelixpg  6820  ixpsnf1o  6822  domen  6839  isfi  6851  en1  6890  xpsnen  6915  xpcomco  6920  xpassen  6924  ssenen  6947  nneneq  6953  snnen2oprc  6956  ac6sfi  6994  exmidpw  7004  exmidpweq  7005  pw1dc1  7010  eldju  7169  djur  7170  eldju2ndl  7173  eldju2ndr  7174  finomni  7241  nninfwlporlemd  7273  nninfwlpoimlemg  7276  acfun  7318  pw1nel3  7342  sucpw1nel3  7344  ccfunen  7375  elni  7420  ltexpi  7449  enq0enq  7543  enq0ref  7545  enq0tr  7546  prarloclem3  7609  ltdfpr  7618  genpdflem  7619  genpassl  7636  genpassu  7637  nqprrnd  7655  nqprl  7663  nqpru  7664  ltexprlemopl  7713  ltexprlemopu  7715  ltexprlemdisj  7718  ltexprlemloc  7719  recexprlemdisj  7742  caucvgprprlemell  7797  caucvgprprlemelu  7798  suplocexprlemml  7828  suplocsrlemb  7918  opelcn  7938  elreal  7940  elreal2  7942  peano1nnnn  7964  axicn  7975  axaddf  7980  axmulf  7981  axprecex  7992  axpre-ltirr  7994  axpre-mulgt0  7999  axcaucvglemres  8011  axpre-suploc  8014  xrlenlt  8136  ltxrlt  8137  inelr  8656  reapcotr  8670  1nn  9046  elnnne0  9308  un0addcl  9327  un0mulcl  9328  elnnz  9381  elznn0nn  9385  elznn0  9386  elznn  9387  elz2  9443  zapne  9446  3halfnz  9469  prime  9471  raluz2  9699  rexuz2  9701  supinfneg  9715  infsupneg  9716  eluz2b2  9723  eluz2b3  9724  ublbneg  9733  elq  9742  qreccl  9762  elpq  9769  ralrp  9796  rexrp  9797  rpnegap  9807  ltxr  9896  xrnemnf  9898  xrltso  9917  icc0r  10047  divelunit  10123  fzprval  10203  fztpval  10204  elfz1b  10211  fz01or  10232  4fvwrd4  10261  fzolb  10275  fzolb2  10276  elfzo3  10285  fzouzsplit  10301  elfzo0z  10306  fzo0m  10313  fzind2  10366  ioo0  10400  ico0  10402  ioc0  10403  uzennn  10579  seq3f1olemp  10658  iswrd  10994  caucvgre  11234  cvg1nlemcau  11237  resqrexlemex  11278  climeu  11549  fsum2dlemstep  11687  expcnv  11757  prodsnf  11845  fprod2dlemstep  11875  divides  12042  m1exp1  12154  divalgb  12178  bitsval2  12197  bitsmod  12209  bitscmp  12211  bezoutlemnewy  12259  bezoutlemmain  12261  bezoutlemex  12264  dfgcd2  12277  nnwosdc  12302  lcmgcdlem  12341  isprm2  12381  isprm3  12382  isprm4  12383  isprm5  12406  sqrt2irr  12426  oddpwdc  12438  pythagtriplem19  12547  pythagtrip  12548  pceu  12560  dvdsprmpweqnn  12601  4sqlem2  12654  4sqlem12  12667  dec5dvds2  12678  ennnfoneleminc  12724  ennnfonelemex  12727  ennnfonelemr  12736  ctiunct  12753  infpn2  12769  xpsfrnel  13118  xpsfrnel2  13120  gsum0g  13170  ismnd  13193  dfgrp2e  13302  dfgrp3me  13374  isnsg2  13481  eqger  13502  isabl2  13572  imasabl  13614  isrhm  13862  isrim  13873  isnzr2  13888  lss1d  14087  istps  14446  istps2  14447  isbasis2g  14459  tgval2  14465  txuni2  14670  tx1cn  14683  tx2cn  14684  uptx  14688  txdis1cn  14692  blres  14848  xmeterval  14849  xmeter  14850  isxms2  14866  isms2  14868  metrest  14920  qtopbasss  14935  dedekindicclemicc  15046  limcdifap  15076  plyrecj  15177  pilem1  15193  sincosq1lem  15239  mpodvdsmulf1o  15404  gausslemma2dlem1a  15477  gausslemma2dlem4  15483  lgsquadlem1  15496  lgsquadlem2  15497  2lgslem1b  15508  2sqlem1  15533  decidr  15665  bdcuni  15745  bdcriota  15752  bdinex1  15768  bj-zfpair2  15779  bj-axun2  15784  bj-ssom  15805  ss1oel2o  15861  nninfsellemdc  15880  nninfsellemsuc  15882  nninfsellemqall  15885  trirec0xor  15917  iswomni0  15923