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  684  mt2bi  686  orbi12i  766  or42  774  pm5.53  804  orddi  822  anddi  823  pm2.1dc  839  dcim  843  notnotrdc  845  dcnnOLD  851  rbaib  923  rbaibr  924  pm4.43  952  orbididc  956  pm5.75  965  3orass  984  3anass  985  3ancomb  989  3anan32  992  3anan12  993  anandi3  994  anandi3r  995  xordc  1412  falbitru  1437  19.26-2  1506  19.26-3an  1507  alrot3  1509  albiim  1511  2albiim  1512  19.27h  1584  19.27  1585  19.28h  1586  19.28  1587  nfalt  1602  aaanh  1610  aaan  1611  alinexa  1627  19.21-2  1691  nf2  1692  19.44  1706  19.45  1707  exrot3  1714  exrot4  1715  eeor  1719  sbcof2  1834  sbid2h  1873  19.23vv  1908  sbnv  1913  sblimv  1919  pm11.53  1920  19.41vv  1928  19.41vvv  1929  19.41vvvv  1930  exdistrv  1935  19.42vv  1936  19.42vvv  1937  19.42vvvv  1938  4exdistr  1941  cbvex4v  1959  eean  1960  sbn  1981  sbim  1982  sbor  1983  sban  1984  sbrim  1985  sblim  1986  sbbi  1988  sblbis  1989  sbrbis  1990  sbrbif  1991  sbco2d  1995  sbco2vd  1996  sbnf2  2010  2sb5  2012  2sb6  2013  sbcom2v  2014  sbcom2v2  2015  sbcom2  2016  sb6a  2017  2sb5rf  2018  2sb6rf  2019  sbalyz  2028  sbal  2029  sbal1yz  2030  sbex  2033  sbalv  2034  sbco4lem  2035  exsb  2037  2exsb  2038  eujust  2057  euf  2060  cbveu  2079  mor  2097  eu2  2099  mo4f  2115  eu4  2117  2exeu  2147  2eu4  2148  exists1  2151  abid  2194  eleq12i  2274  abeq2  2315  abeq2i  2317  clabel  2333  abid2f  2375  sbabel  2376  neeq12i  2394  neanior  2464  ralnex  2495  dfrex2dc  2498  ralinexa  2534  nfraldya  2542  nfrexdya  2543  r3al  2551  r19.26-2  2636  ralbiim  2641  ralnex2  2646  r19.43  2665  ralcomf  2668  rexcomf  2669  ralrot3  2672  rexrot4  2674  reean  2676  3reeanv  2678  rabbi  2685  cbvralf  2731  cbvrexf  2732  cbvreu  2737  cbvral2vw  2750  cbvrex2vw  2751  cbvral2v  2752  cbvrex2v  2753  cbvral3v  2754  cbvralsv  2755  cbvrexsv  2756  sbralie  2757  rabeq2i  2770  issetf  2781  2gencl  2807  3gencl  2808  ceqsex2  2815  ceqsex3v  2817  ceqsex6v  2819  ceqsex8v  2820  gencbvex  2821  gencbval  2823  spc2gv  2868  eqvincf  2902  ceqsrex2v  2909  clel5  2914  elrab2  2936  ralab  2937  ralrab  2938  rexab  2939  rexrab  2940  ralab2  2941  rexab2  2943  eueq3dc  2951  morex  2961  euind  2964  reu2  2965  reu6  2966  rmo4  2970  reu4  2971  reu7  2972  rmo3f  2974  rmo4f  2975  rmoim  2978  2reuswapdc  2981  reuind  2982  2rmorex  2983  sbcco  3024  sbccomlem  3077  sbccom  3078  ra5  3091  rmo3  3094  csbco  3107  csbcow  3108  sbnfc2  3158  csbabg  3159  cbvralcsf  3160  cbvrexcsf  3161  cbvreucsf  3162  dfss  3184  dfss2f  3188  ss2ab  3265  dfdif3  3287  difeqri  3297  ddifstab  3309  raldifb  3317  uneqri  3319  ssequn2  3350  unss  3351  rexun  3357  ralunb  3358  elin2  3365  ineqri  3370  dfss1  3381  dfss5  3382  dfss4st  3410  ssddif  3411  difin  3414  indif  3420  difundi  3429  indifdir  3433  symdifxor  3443  inrab2  3450  rabun2  3456  reuun2  3460  0el  3487  rabeq0  3494  abeq0  3495  disjr  3514  disj1  3515  undif4  3527  uneqdifeqim  3550  r19.2m  3551  r19.3rm  3553  r19.9rmv  3556  raaan  3570  pwss  3637  dfpr2  3657  rexdifpr  3666  ralsnsg  3675  ralsns  3676  eltpg  3683  eldiftp  3684  ralprg  3689  rexprg  3690  raltpg  3691  rextpg  3692  snprc  3703  rabrsndc  3706  euabsn2  3707  eusn  3712  eldifsn  3766  ssdifsn  3767  rexdifsn  3771  eqsnm  3802  tpss  3805  snsssn  3808  prel12  3818  preqsn  3822  oprcl  3849  pwtpss  3853  eluniab  3868  elunirab  3869  unipr  3870  dfnfc2  3874  uniun  3875  uniin  3876  uni0b  3881  unissb  3886  elintab  3902  elintrab  3903  ssintab  3908  ssintrab  3914  intun  3922  intpr  3923  elrint  3931  iuncom4  3940  iuneq2  3949  dfiun2g  3965  ssiinf  3983  iundif2ss  3999  elriin  4004  iunxiun  4015  pwssb  4019  elpwpw  4020  iunpwss  4025  dfdisj2  4029  disjiun  4046  cbvopab1  4125  dftr5  4153  trint  4165  inex1  4186  inuni  4207  repizf2lem  4213  unidif0  4219  axpweq  4223  bnd2  4225  exmid01  4250  zfpair2  4262  exss  4279  elop  4283  opm  4286  otth  4294  copsex4g  4299  opeqsn  4305  opelopabsbALT  4313  brabga  4318  opelopabaf  4328  iunopab  4336  pwunss  4338  pocl  4358  frirrg  4405  elsuci  4458  elsucg  4459  sucel  4465  unisucg  4469  uniuni  4506  reusv3  4515  iunpw  4535  setindel  4594  elirr  4597  en2lp  4610  ordpwsucss  4623  zfregfr  4630  tfi  4638  peano2  4651  peano5  4654  elxp  4700  opelxp  4713  brxp  4714  rabxp  4720  opthprc  4734  brab2a  4736  opeliunxp  4738  xpundi  4739  xpundir  4740  elvvv  4746  brinxp  4751  brab2ga  4758  0xp  4763  ssrel2  4773  eqrelrel  4784  reliun  4804  reluni  4806  raliunxp  4827  rexiunxp  4828  ralxpf  4832  rexxpf  4833  iunxpf  4834  relop  4836  elco  4852  elcnv  4863  elcnv2  4864  dmin  4895  dmuni  4897  dmopab  4898  dmi  4902  dmmrnm  4906  rnopab  4934  elrnmpt1  4938  rncoeq  4961  resiexg  5013  restidsing  5024  dfima2  5033  dfima3  5034  elima2  5037  elima3  5038  imai  5047  elimasn  5058  epini  5062  dfse2  5064  cotr  5073  issref  5074  intasym  5076  asymref  5077  cnvopab  5093  cnvi  5096  cnvdif  5098  imainss  5107  rnxpid  5126  dfrel2  5142  dfrel3  5149  dmsnm  5157  rnsnm  5158  relsn2m  5162  dmsnopg  5163  cnvcnvsn  5168  elxp4  5179  elxp5  5180  cnvresima  5181  mptpreima  5185  dfco2  5191  coundi  5193  coundir  5194  imaco  5197  coiun  5201  coi1  5207  relssdmrn  5212  relrelss  5218  unixpm  5227  ressn  5232  cnviinm  5233  cnvpom  5234  cnvsom  5235  cbviota  5246  iotass  5258  eliota  5268  dffun2  5290  dffun4  5291  dffun7  5307  dffun8  5308  dffun9  5309  funopab  5315  funun  5324  funcnvsn  5328  fntpg  5339  funcnv2  5343  funcnv  5344  fun2cnv  5347  fncnv  5349  fun11  5350  fununi  5351  imadiflem  5362  imadif  5363  imainlem  5364  funimaexglem  5366  fnunsn  5392  fnres  5402  fnopabg  5409  mptfng  5411  mptun  5417  fun  5459  fcnvres  5471  dff12  5492  f1cnvcnv  5504  funforn  5517  dff1o2  5539  dff1o5  5543  f1orn  5544  resdif  5556  ffoss  5566  f11o  5567  f1o00  5570  fo00  5571  elfv  5587  fv3  5612  nfvres  5623  eqfnfv3  5692  fneqeql  5701  unpreima  5718  respreima  5721  dffo3  5740  dffo5  5742  f1ompt  5744  ffnfvf  5752  fmptco  5759  funopdmsn  5777  ftpg  5781  fnressn  5783  idref  5838  abrexco  5841  dff13  5850  dff13f  5852  fliftel  5875  isoini  5900  eusvobj2  5943  acexmidlema  5948  acexmidlemb  5949  acexmidlemph  5950  acexmidlem2  5954  oprabid  5989  brabvv  6004  dfoprab2  6005  eqoprab2b  6016  dmoprab  6039  rnoprab  6041  eloprabga  6045  mpomptx  6049  resoprab  6054  ffnov  6062  elrnmpo  6072  ralrnmpo  6073  rexrnmpo  6074  ovid  6075  ovi3  6096  ov6g  6097  foov  6106  opabex3d  6219  opabex3  6220  abexssex  6223  oprabex3  6227  oprabrexex2  6228  fmpo  6300  xporderlem  6330  f1od2  6334  mpoxopovel  6340  brtpos2  6350  dmtpos  6355  tpostpos  6363  tpossym  6375  tposoprab  6379  dfsmo2  6386  tfrlem7  6416  tfrlem9  6418  tfr1onlemaccex  6447  tfrcllemaccex  6460  tfrcldm  6462  frecabex  6497  el1o  6536  dif1o  6537  dfer2  6634  brdifun  6660  eqerlem  6664  qsid  6700  iinerm  6707  riinerm  6708  erinxp  6709  brecop  6725  eroveu  6726  erovlem  6727  ecopovsym  6731  mapval2  6778  mapsn  6790  elixp  6805  ixpeq2  6812  ixpin  6823  ixpiinm  6824  mptelixpg  6834  ixpsnf1o  6836  domen  6853  isfi  6865  en1  6904  xpsnen  6931  xpcomco  6936  xpassen  6940  ssenen  6963  nneneq  6969  snnen2oprc  6972  ac6sfi  7010  exmidpw  7020  exmidpweq  7021  pw1dc1  7026  eldju  7185  djur  7186  eldju2ndl  7189  eldju2ndr  7190  finomni  7257  nninfwlporlemd  7289  nninfwlpoimlemg  7292  acfun  7335  pw1nel3  7362  sucpw1nel3  7364  ccfunen  7396  elni  7441  ltexpi  7470  enq0enq  7564  enq0ref  7566  enq0tr  7567  prarloclem3  7630  ltdfpr  7639  genpdflem  7640  genpassl  7657  genpassu  7658  nqprrnd  7676  nqprl  7684  nqpru  7685  ltexprlemopl  7734  ltexprlemopu  7736  ltexprlemdisj  7739  ltexprlemloc  7740  recexprlemdisj  7763  caucvgprprlemell  7818  caucvgprprlemelu  7819  suplocexprlemml  7849  suplocsrlemb  7939  opelcn  7959  elreal  7961  elreal2  7963  peano1nnnn  7985  axicn  7996  axaddf  8001  axmulf  8002  axprecex  8013  axpre-ltirr  8015  axpre-mulgt0  8020  axcaucvglemres  8032  axpre-suploc  8035  xrlenlt  8157  ltxrlt  8158  inelr  8677  reapcotr  8691  1nn  9067  elnnne0  9329  un0addcl  9348  un0mulcl  9349  elnnz  9402  elznn0nn  9406  elznn0  9407  elznn  9408  elz2  9464  zapne  9467  3halfnz  9490  prime  9492  raluz2  9720  rexuz2  9722  supinfneg  9736  infsupneg  9737  eluz2b2  9744  eluz2b3  9745  ublbneg  9754  elq  9763  qreccl  9783  elpq  9790  ralrp  9817  rexrp  9818  rpnegap  9828  ltxr  9917  xrnemnf  9919  xrltso  9938  icc0r  10068  divelunit  10144  fzprval  10224  fztpval  10225  elfz1b  10232  fz01or  10253  4fvwrd4  10282  fzolb  10296  fzolb2  10297  elfzo3  10306  fzouzsplit  10323  elfzo0z  10330  fzo0m  10337  fzind2  10390  ioo0  10424  ico0  10426  ioc0  10427  uzennn  10603  seq3f1olemp  10682  iswrd  11018  caucvgre  11367  cvg1nlemcau  11370  resqrexlemex  11411  climeu  11682  fsum2dlemstep  11820  expcnv  11890  prodsnf  11978  fprod2dlemstep  12008  divides  12175  m1exp1  12287  divalgb  12311  bitsval2  12330  bitsmod  12342  bitscmp  12344  bezoutlemnewy  12392  bezoutlemmain  12394  bezoutlemex  12397  dfgcd2  12410  nnwosdc  12435  lcmgcdlem  12474  isprm2  12514  isprm3  12515  isprm4  12516  isprm5  12539  sqrt2irr  12559  oddpwdc  12571  pythagtriplem19  12680  pythagtrip  12681  pceu  12693  dvdsprmpweqnn  12734  4sqlem2  12787  4sqlem12  12800  dec5dvds2  12811  ennnfoneleminc  12857  ennnfonelemex  12860  ennnfonelemr  12869  ctiunct  12886  infpn2  12902  xpsfrnel  13251  xpsfrnel2  13253  gsum0g  13303  ismnd  13326  dfgrp2e  13435  dfgrp3me  13507  isnsg2  13614  eqger  13635  isabl2  13705  imasabl  13747  isrhm  13995  isrim  14006  isnzr2  14021  lss1d  14220  istps  14579  istps2  14580  isbasis2g  14592  tgval2  14598  txuni2  14803  tx1cn  14816  tx2cn  14817  uptx  14821  txdis1cn  14825  blres  14981  xmeterval  14982  xmeter  14983  isxms2  14999  isms2  15001  metrest  15053  qtopbasss  15068  dedekindicclemicc  15179  limcdifap  15209  plyrecj  15310  pilem1  15326  sincosq1lem  15372  mpodvdsmulf1o  15537  gausslemma2dlem1a  15610  gausslemma2dlem4  15616  lgsquadlem1  15629  lgsquadlem2  15630  2lgslem1b  15641  2sqlem1  15666  upgrex  15774  decidr  15871  bdcuni  15950  bdcriota  15957  bdinex1  15973  bj-zfpair2  15984  bj-axun2  15989  bj-ssom  16010  ss1oel2o  16066  nninfsellemdc  16088  nninfsellemsuc  16090  nninfsellemqall  16093  trirec0xor  16125  iswomni0  16131