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  1858  sbid2h  1897  19.23vv  1932  sbnv  1937  sblimv  1943  pm11.53  1944  19.41vv  1952  19.41vvv  1953  19.41vvvv  1954  exdistrv  1959  19.42vv  1960  19.42vvv  1961  19.42vvvv  1962  4exdistr  1965  cbvex4v  1983  eean  1984  sbn  2005  sbim  2006  sbor  2007  sban  2008  sbrim  2009  sblim  2010  sbbi  2012  sblbis  2013  sbrbis  2014  sbrbif  2015  sbco2d  2019  sbco2vd  2020  sbnf2  2034  2sb5  2036  2sb6  2037  sbcom2v  2038  sbcom2v2  2039  sbcom2  2040  sb6a  2041  2sb5rf  2042  2sb6rf  2043  sbalyz  2052  sbal  2053  sbal1yz  2054  sbex  2057  sbalv  2058  sbco4lem  2059  exsb  2061  2exsb  2062  eujust  2081  euf  2084  cbveu  2103  mor  2122  eu2  2124  mo4f  2140  eu4  2142  2exeu  2172  2eu4  2173  exists1  2176  abid  2219  eleq12i  2299  abeq2  2340  abeq2i  2342  abbib  2349  clabel  2359  abid2f  2401  sbabel  2402  neeq12i  2420  neanior  2490  ralnex  2521  dfrex2dc  2524  ralinexa  2560  nfraldya  2568  nfrexdya  2569  r3al  2577  r19.26-2  2663  ralbiim  2668  ralnex2  2673  r19.43  2692  ralcomf  2695  rexcomf  2696  ralrot3  2699  rexrot4  2701  reean  2703  3reeanv  2705  rabbi  2712  cbvralf  2759  cbvrexf  2760  cbvreu  2766  cbvral2vw  2779  cbvrex2vw  2780  cbvral2v  2781  cbvrex2v  2782  cbvral3v  2783  cbvralsv  2784  cbvrexsv  2785  sbralie  2786  rabeq2i  2800  issetf  2811  2gencl  2837  3gencl  2838  ceqsex2  2845  ceqsex3v  2847  ceqsex6v  2849  ceqsex8v  2850  gencbvex  2851  gencbval  2853  spc2gv  2898  eqvincf  2932  ceqsrex2v  2939  clel5  2944  elrab2  2966  ralab  2967  ralrab  2968  rexab  2969  rexrab  2970  ralab2  2971  rexab2  2973  eueq3dc  2981  morex  2991  euind  2994  reu2  2995  reu6  2996  rmo4  3000  reu4  3001  reu7  3002  rmo3f  3004  rmo4f  3005  rmoim  3008  2reuswapdc  3011  reuind  3012  2rmorex  3013  sbcco  3054  sbccomlem  3107  sbccom  3108  ra5  3122  rmo3  3125  csbco  3138  csbcow  3139  sbnfc2  3189  csbabg  3190  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  dfss  3215  dfss2f  3219  ss2ab  3296  dfdif3  3319  difeqri  3329  ddifstab  3341  raldifb  3349  uneqri  3351  ssequn2  3382  unss  3383  rexun  3389  ralunb  3390  elin2  3397  ineqri  3402  dfss1  3413  dfss5  3414  dfss4st  3442  ssddif  3443  difin  3446  indif  3452  difundi  3461  indifdir  3465  symdifxor  3475  inrab2  3482  rabun2  3488  reuun2  3492  0el  3519  rabeq0  3526  abeq0  3527  disjr  3546  disj1  3547  undif4  3559  uneqdifeqim  3582  r19.2m  3583  r19.3rm  3585  r19.9rmv  3588  raaan  3602  pwss  3672  dfpr2  3692  rexdifpr  3701  ralsnsg  3710  ralsns  3711  eltpg  3718  eldiftp  3719  ralprg  3724  rexprg  3725  raltpg  3726  rextpg  3727  snprc  3738  rabrsndc  3743  euabsn2  3744  eusn  3749  eldifsn  3804  ssdifsn  3805  rexdifsn  3809  eqsnm  3843  tpss  3846  snsssn  3849  prel12  3859  preqsn  3863  oprcl  3891  pwtpss  3895  eluniab  3910  elunirab  3911  unipr  3912  dfnfc2  3916  uniun  3917  uniin  3918  uni0b  3923  unissb  3928  elintab  3944  elintrab  3945  ssintab  3950  ssintrab  3956  intun  3964  intpr  3965  elrint  3973  iuncom4  3982  iuneq2  3991  dfiun2g  4007  ssiinf  4025  iundif2ss  4041  elriin  4046  iunxiun  4057  pwssb  4061  elpwpw  4062  iunpwss  4067  dfdisj2  4071  disjiun  4088  cbvopab1  4167  dftr5  4195  trint  4207  inex1  4228  inuni  4250  repizf2lem  4257  unidif0  4263  axpweq  4267  bnd2  4269  exmid01  4294  zfpair2  4306  exss  4325  elop  4329  opm  4332  otth  4340  copsex4g  4345  opeqsn  4351  opelopabsbALT  4359  brabga  4364  opelopabaf  4374  iunopab  4382  pwunss  4386  pocl  4406  frirrg  4453  elsuci  4506  elsucg  4507  sucel  4513  unisucg  4517  uniuni  4554  reusv3  4563  iunpw  4583  setindel  4642  elirr  4645  en2lp  4658  ordpwsucss  4671  zfregfr  4678  tfi  4686  peano2  4699  peano5  4702  elxp  4748  opelxp  4761  brxp  4762  rabxp  4769  opthprc  4783  brab2a  4785  opeliunxp  4787  xpundi  4788  xpundir  4789  elvvv  4795  brinxp  4800  brab2ga  4807  0xp  4812  ssrel2  4822  eqrelrel  4833  reliun  4854  reluni  4856  raliunxp  4877  rexiunxp  4878  ralxpf  4882  rexxpf  4883  iunxpf  4884  relop  4886  elco  4902  elcnv  4913  elcnv2  4914  dmin  4945  dmuni  4947  dmopab  4948  dmi  4952  dmmrnm  4957  rnopab  4985  elrnmpt1  4989  rncoeq  5012  resiexg  5064  restidsing  5075  dfima2  5084  dfima3  5085  elima2  5088  elima3  5089  imai  5099  elimasn  5110  epini  5114  dfse2  5116  cotr  5125  issref  5126  intasym  5128  asymref  5129  cnvopab  5145  cnvi  5148  cnvdif  5150  imainss  5159  rnxpid  5178  dfrel2  5194  dfrel3  5201  dmsnm  5209  rnsnm  5210  relsn2m  5214  dmsnopg  5215  cnvcnvsn  5220  elxp4  5231  elxp5  5232  cnvresima  5233  mptpreima  5237  dfco2  5243  coundi  5245  coundir  5246  imaco  5249  coiun  5253  coi1  5259  relssdmrn  5264  relrelss  5270  unixpm  5279  ressn  5284  cnviinm  5285  cnvpom  5286  cnvsom  5287  cbviota  5298  iotass  5311  eliota  5321  dffun2  5343  dffun4  5344  dffun7  5360  dffun8  5361  dffun9  5362  funopab  5368  funun  5378  funcnvsn  5382  fntpg  5393  funcnv2  5397  funcnv  5398  fun2cnv  5401  fncnv  5403  fun11  5404  fununi  5405  imadiflem  5416  imadif  5417  imainlem  5418  funimaexglem  5420  fnunsn  5446  fnres  5456  fnopabg  5463  mptfng  5465  mptun  5471  fun  5516  fcnvres  5528  dff12  5550  f1cnvcnv  5562  funforn  5575  dff1o2  5597  dff1o5  5601  f1orn  5602  resdif  5614  ffoss  5625  f11o  5626  f1o00  5629  fo00  5630  elfv  5646  fv3  5671  nfvres  5684  eqfnfv3  5755  fneqeql  5764  unpreima  5780  respreima  5783  dffo3  5802  dffo5  5804  f1ompt  5806  ffnfvf  5814  fmptco  5821  funopdmsn  5842  ftpg  5846  fnressn  5848  idref  5907  abrexco  5910  dff13  5919  dff13f  5921  fliftel  5944  isoini  5969  eusvobj2  6014  acexmidlema  6019  acexmidlemb  6020  acexmidlemph  6021  acexmidlem2  6025  oprabid  6060  brabvv  6077  dfoprab2  6078  eqoprab2b  6089  dmoprab  6112  rnoprab  6114  eloprabga  6118  mpomptx  6122  resoprab  6127  ffnov  6135  elrnmpo  6145  ralrnmpo  6146  rexrnmpo  6147  ovid  6148  ovi3  6169  ov6g  6170  foov  6179  opabex3d  6292  opabex3  6293  abexssex  6296  oprabex3  6300  oprabrexex2  6301  fmpo  6375  xporderlem  6405  f1od2  6409  mpoxopovel  6450  brtpos2  6460  dmtpos  6465  tpostpos  6473  tpossym  6485  tposoprab  6489  dfsmo2  6496  tfrlem7  6526  tfrlem9  6528  tfr1onlemaccex  6557  tfrcllemaccex  6570  tfrcldm  6572  frecabex  6607  el1o  6648  dif1o  6649  dfer2  6746  brdifun  6772  eqerlem  6776  qsid  6812  iinerm  6819  riinerm  6820  erinxp  6821  brecop  6837  eroveu  6838  erovlem  6839  ecopovsym  6843  mapval2  6890  mapsn  6902  elixp  6917  ixpeq2  6924  ixpin  6935  ixpiinm  6936  mptelixpg  6946  ixpsnf1o  6948  domen  6965  isfi  6977  en1  7016  modom2  7038  xpsnen  7048  xpcomco  7053  xpassen  7057  ssenen  7080  nneneq  7086  snnen2oprc  7089  ac6sfi  7130  exmidpw  7143  exmidpweq  7144  pw1dc1  7149  eldju  7310  djur  7311  eldju2ndl  7314  eldju2ndr  7315  finomni  7382  nninfwlporlemd  7414  nninfwlpoimlemg  7417  acfun  7465  pw1nel3  7492  sucpw1nel3  7494  ccfunen  7526  elni  7571  ltexpi  7600  enq0enq  7694  enq0ref  7696  enq0tr  7697  prarloclem3  7760  ltdfpr  7769  genpdflem  7770  genpassl  7787  genpassu  7788  nqprrnd  7806  nqprl  7814  nqpru  7815  ltexprlemopl  7864  ltexprlemopu  7866  ltexprlemdisj  7869  ltexprlemloc  7870  recexprlemdisj  7893  caucvgprprlemell  7948  caucvgprprlemelu  7949  suplocexprlemml  7979  suplocsrlemb  8069  opelcn  8089  elreal  8091  elreal2  8093  peano1nnnn  8115  axicn  8126  axaddf  8131  axmulf  8132  axprecex  8143  axpre-ltirr  8145  axpre-mulgt0  8150  axcaucvglemres  8162  axpre-suploc  8165  xrlenlt  8286  ltxrlt  8287  inelr  8806  reapcotr  8820  1nn  9196  elnnne0  9458  un0addcl  9477  un0mulcl  9478  elnnz  9533  elznn0nn  9537  elznn0  9538  elznn  9539  elz2  9595  zapne  9598  3halfnz  9621  prime  9623  raluz2  9857  rexuz2  9859  supinfneg  9873  infsupneg  9874  eluz2b2  9881  eluz2b3  9882  ublbneg  9891  elq  9900  qreccl  9920  elpq  9927  ralrp  9954  rexrp  9955  rpnegap  9965  ltxr  10054  xrnemnf  10056  xrltso  10075  icc0r  10205  divelunit  10281  fzprval  10362  fztpval  10363  elfz1b  10370  fz01or  10391  4fvwrd4  10420  fzolb  10434  fzolb2  10435  elfzo3  10444  fzouzsplit  10461  elfzo0z  10469  fzo0m  10477  fzind2  10531  ioo0  10565  ico0  10567  ioc0  10568  uzennn  10744  seq3f1olemp  10823  iswrd  11164  caucvgre  11604  cvg1nlemcau  11607  resqrexlemex  11648  climeu  11919  fsum2dlemstep  12058  expcnv  12128  prodsnf  12216  fprod2dlemstep  12246  divides  12413  m1exp1  12525  divalgb  12549  bitsval2  12568  bitsmod  12580  bitscmp  12582  bezoutlemnewy  12630  bezoutlemmain  12632  bezoutlemex  12635  dfgcd2  12648  nnwosdc  12673  lcmgcdlem  12712  isprm2  12752  isprm3  12753  isprm4  12754  isprm5  12777  sqrt2irr  12797  oddpwdc  12809  pythagtriplem19  12918  pythagtrip  12919  pceu  12931  dvdsprmpweqnn  12972  4sqlem2  13025  4sqlem12  13038  dec5dvds2  13049  ennnfoneleminc  13095  ennnfonelemex  13098  ennnfonelemr  13107  ctiunct  13124  infpn2  13140  xpsfrnel  13490  xpsfrnel2  13492  gsum0g  13542  ismnd  13565  dfgrp2e  13674  dfgrp3me  13746  isnsg2  13853  eqger  13874  isabl2  13944  imasabl  13986  isrhm  14236  isrim  14247  isnzr2  14262  lss1d  14462  istps  14826  istps2  14827  isbasis2g  14839  tgval2  14845  txuni2  15050  tx1cn  15063  tx2cn  15064  uptx  15068  txdis1cn  15072  blres  15228  xmeterval  15229  xmeter  15230  isxms2  15246  isms2  15248  metrest  15300  qtopbasss  15315  dedekindicclemicc  15426  limcdifap  15456  plyrecj  15557  pilem1  15573  sincosq1lem  15619  mpodvdsmulf1o  15787  gausslemma2dlem1a  15860  gausslemma2dlem4  15866  lgsquadlem1  15879  lgsquadlem2  15880  2lgslem1b  15891  2sqlem1  15916  upgrex  16027  griedg0ssusgr  16175  clwwlkn1loopb  16344  clwwlknon2x  16359  decidr  16497  bdcuni  16575  bdcriota  16582  bdinex1  16598  bj-zfpair2  16609  bj-axun2  16614  bj-ssom  16635  ss1oel2o  16690  nninfsellemdc  16719  nninfsellemsuc  16721  nninfsellemqall  16724  trirec0xor  16760  iswomni0  16767