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  1938  sblimv  1944  pm11.53  1945  19.41vv  1953  19.41vvv  1954  19.41vvvv  1955  exdistrv  1960  19.42vv  1961  19.42vvv  1962  19.42vvvv  1963  4exdistr  1966  cbvex4v  1984  eean  1985  sbn  2006  sbim  2007  sbor  2008  sban  2009  sbrim  2010  sblim  2011  sbbi  2013  sblbis  2014  sbrbis  2015  sbrbif  2016  sbco2d  2020  sbco2vd  2021  sbnf2  2035  2sb5  2037  2sb6  2038  sbcom2v  2039  sbcom2v2  2040  sbcom2  2041  sb6a  2042  2sb5rf  2043  2sb6rf  2044  sbalyz  2053  sbal  2054  sbal1yz  2055  sbex  2058  sbalv  2059  sbco4lem  2060  exsb  2062  2exsb  2063  eujust  2082  euf  2085  cbveu  2104  mor  2123  eu2  2125  mo4f  2141  eu4  2143  2exeu  2173  2eu4  2174  exists1  2177  abid  2220  eleq12i  2300  abeq2  2341  abeq2i  2343  abbib  2350  clabel  2361  eqabb  2368  abid2f  2410  sbabel  2411  neeq12i  2429  neanior  2499  ralnex  2530  dfrex2dc  2533  ralinexa  2569  nfraldya  2577  nfrexdya  2578  r3al  2586  r19.26-2  2672  ralbiim  2677  ralnex2  2682  r19.43  2701  ralcomf  2704  rexcomf  2705  ralrot3  2708  rexrot4  2710  reean  2712  3reeanv  2714  reqabi  2720  rabbi  2722  cbvralf  2769  cbvrexf  2770  cbvreu  2776  cbvral2vw  2789  cbvrex2vw  2790  cbvral2v  2791  cbvrex2v  2792  cbvral3v  2793  cbvralsv  2794  cbvrexsv  2795  sbralie  2796  rabeq2i  2810  issetf  2821  2gencl  2847  3gencl  2848  ceqsex2  2855  ceqsex3v  2857  ceqsex6v  2859  ceqsex8v  2860  gencbvex  2861  gencbval  2863  spc2gv  2908  eqvincf  2942  ceqsrex2v  2949  clel5  2954  elrab2  2976  ralab  2977  ralrab  2978  rexab  2979  rexrab  2980  ralab2  2981  rexab2  2983  eueq3dc  2991  morex  3001  euind  3004  reu2  3005  reu6  3006  rmo4  3010  reu4  3011  reu7  3012  rmo3f  3014  rmo4f  3015  rmoim  3018  2reuswapdc  3021  reuind  3022  2rmorex  3023  sbcco  3064  sbccomlem  3117  sbccom  3118  ra5  3132  rmo3  3135  csbco  3148  csbcow  3149  sbnfc2  3199  csbabg  3200  cbvralcsf  3201  cbvrexcsf  3202  cbvreucsf  3203  dfss  3225  dfss2f  3229  ss2ab  3306  dfdif3  3329  difeqri  3339  ddifstab  3351  raldifb  3359  uneqri  3361  ssequn2  3392  unss  3393  rexun  3399  ralunb  3400  elin2  3407  ineqri  3414  dfss1  3425  dfss5  3426  dfss4st  3454  ssddif  3455  difin  3458  indif  3464  difundi  3473  indifdir  3477  symdifxor  3487  inrab2  3494  rabun2  3500  reuun2  3504  0el  3531  rabeq0  3538  abeq0  3539  disjr  3558  disj1  3559  undif4  3571  uneqdifeqim  3595  r19.2m  3596  r19.3rm  3598  r19.9rmv  3601  raaan  3615  pwss  3688  dfpr2  3708  rexdifpr  3717  ralsnsg  3726  ralsns  3727  eltpg  3734  eldiftp  3735  ralprg  3740  rexprg  3741  raltpg  3742  rextpg  3743  snprc  3754  rabrsndc  3759  euabsn2  3760  eusn  3765  eldifsn  3820  ssdifsn  3821  rexdifsn  3825  eqsnm  3859  tpss  3862  snsssn  3865  prel12  3875  preqsn  3879  oprcl  3907  pwtpss  3911  eluniab  3926  elunirab  3927  unipr  3928  dfnfc2  3932  uniun  3933  uniin  3934  uni0b  3939  unissb  3944  elintab  3960  elintrab  3961  ssintab  3966  ssintrab  3972  intun  3980  intpr  3981  elrint  3989  iuncom4  3998  iuneq2  4007  dfiun2g  4023  ssiinf  4041  iundif2ss  4057  elriin  4062  iunxiun  4073  pwssb  4077  elpwpw  4078  iunpwss  4083  dfdisj2  4087  disjiun  4104  cbvopab1  4183  dftr5  4211  trint  4223  inex1  4244  inuni  4267  repizf2lem  4274  unidif0  4280  axpweq  4284  bnd2  4286  exmid01  4311  zfpair2  4323  exss  4343  elop  4347  opm  4350  otth  4358  copsex4g  4363  opeqsn  4369  opelopabsbALT  4377  brabga  4382  opelopabaf  4392  iunopab  4400  pwunss  4404  pocl  4424  frirrg  4471  elsuci  4524  elsucg  4525  sucel  4531  unisucg  4535  uniuni  4572  reusv3  4581  iunpw  4601  setindel  4660  elirr  4663  en2lp  4676  ordpwsucss  4689  zfregfr  4696  tfi  4704  peano2  4717  peano5  4720  elxp  4766  opelxp  4779  brxp  4780  rabxp  4787  opthprc  4801  brab2a  4803  opeliunxp  4805  xpundi  4806  xpundir  4807  elvvv  4813  brinxp  4818  brab2ga  4825  0xp  4830  ssrel2  4840  eqrelrel  4851  reliun  4873  reluni  4875  raliunxp  4896  rexiunxp  4897  ralxpf  4901  rexxpf  4902  iunxpf  4903  relop  4905  elco  4921  elcnv  4932  elcnv2  4933  dmin  4964  dmuni  4966  dmopab  4967  dmi  4971  dmmrnm  4976  rnopab  5004  elrnmpt1  5008  rncoeq  5031  resiexg  5083  restidsing  5094  dfima2  5103  dfima3  5104  elima2  5107  elima3  5108  imai  5118  elimasn  5129  epini  5133  dfse2  5135  cotr  5144  issref  5145  intasym  5147  asymref  5148  cnvopab  5164  cnvi  5167  cnvdif  5169  imainss  5178  rnxpid  5197  dfrel2  5213  dfrel3  5220  dmsnm  5228  rnsnm  5229  relsn2m  5233  dmsnopg  5234  cnvcnvsn  5239  elxp4  5250  elxp5  5251  cnvresima  5252  mptpreima  5256  dfco2  5262  coundi  5264  coundir  5265  imaco  5268  coiun  5272  coi1  5278  relssdmrn  5283  relrelss  5289  unixpm  5298  ressn  5303  cnviinm  5304  cnvpom  5305  cnvsom  5306  cbviota  5317  iotass  5330  eliota  5340  dffun2  5362  dffun4  5363  dffun7  5379  dffun8  5380  dffun9  5381  funopab  5387  funun  5397  funcnvsn  5401  fntpg  5412  funcnv2  5416  funcnv  5417  fun2cnv  5420  fncnv  5422  fun11  5423  fununi  5424  imadiflem  5435  imadif  5436  imainlem  5437  funimaexglem  5439  fnunsn  5465  fnres  5475  fnopabg  5482  mptfng  5484  mptun  5490  fun  5536  fcnvres  5550  dff12  5572  f1cnvcnv  5584  funforn  5597  dff1o2  5619  dff1o5  5623  f1orn  5624  resdif  5636  ffoss  5647  f11o  5648  f1o00  5651  fo00  5652  elfv  5668  fv3  5693  nfvres  5706  eqfnfv3  5777  fneqeql  5786  unpreima  5802  respreima  5805  dffo3  5824  dffo5  5826  f1ompt  5828  ffnfvf  5836  fmptco  5843  funopdmsn  5864  ftpg  5868  fnressn  5870  idref  5929  abrexco  5932  dff13  5941  dff13f  5943  fliftel  5966  isoini  5991  eusvobj2  6036  acexmidlema  6041  acexmidlemb  6042  acexmidlemph  6043  acexmidlem2  6047  oprabid  6082  brabvv  6099  dfoprab2  6100  eqoprab2b  6111  dmoprab  6134  rnoprab  6136  eloprabga  6140  mpomptx  6144  resoprab  6149  ffnov  6157  elrnmpo  6167  ralrnmpo  6168  rexrnmpo  6169  ovid  6170  ovi3  6191  ov6g  6192  foov  6201  opabex3d  6314  opabex3  6315  abexssex  6318  oprabex3  6322  oprabrexex2  6323  fmpo  6397  xporderlem  6427  f1od2  6431  mpoxopovel  6472  brtpos2  6482  dmtpos  6487  tpostpos  6495  tpossym  6507  tposoprab  6511  dfsmo2  6518  tfrlem7  6548  tfrlem9  6550  tfr1onlemaccex  6579  tfrcllemaccex  6592  tfrcldm  6594  frecabex  6629  el1o  6670  dif1o  6671  dfer2  6768  brdifun  6794  eqerlem  6798  qsid  6834  iinerm  6841  riinerm  6842  erinxp  6843  brecop  6859  eroveu  6860  erovlem  6861  ecopovsym  6865  mapval2  6912  mapsn  6925  elixp  6940  ixpeq2  6947  ixpin  6958  ixpiinm  6959  mptelixpg  6969  ixpsnf1o  6971  domen  6988  isfi  7000  en1  7039  modom2  7062  xpsnen  7072  xpcomco  7077  xpassen  7081  ssenen  7105  nneneq  7111  snnen2oprc  7114  ac6sfi  7155  exmidpw  7168  exmidpweq  7169  pw1dc1  7174  elfpw  7215  eldju  7359  djur  7360  eldju2ndl  7363  eldju2ndr  7364  finomni  7431  nninfwlporlemd  7463  nninfwlpoimlemg  7466  acfun  7514  pw1nel3  7541  sucpw1nel3  7543  ccfunen  7578  elni  7623  ltexpi  7652  enq0enq  7746  enq0ref  7748  enq0tr  7749  prarloclem3  7812  ltdfpr  7821  genpdflem  7822  genpassl  7839  genpassu  7840  nqprrnd  7858  nqprl  7866  nqpru  7867  ltexprlemopl  7916  ltexprlemopu  7918  ltexprlemdisj  7921  ltexprlemloc  7922  recexprlemdisj  7945  caucvgprprlemell  8000  caucvgprprlemelu  8001  suplocexprlemml  8031  suplocsrlemb  8121  opelcn  8141  elreal  8143  elreal2  8145  peano1nnnn  8167  axicn  8178  axaddf  8183  axmulf  8184  axprecex  8195  axpre-ltirr  8197  axpre-mulgt0  8202  axcaucvglemres  8214  axpre-suploc  8217  xrlenlt  8338  ltxrlt  8339  inelr  8858  reapcotr  8872  1nn  9248  elnnne0  9510  un0addcl  9529  un0mulcl  9530  elnnz  9587  elznn0nn  9591  elznn0  9592  elznn  9593  elz2  9649  zapne  9652  3halfnz  9675  prime  9677  raluz2  9911  rexuz2  9913  supinfneg  9927  infsupneg  9928  eluz2b2  9935  eluz2b3  9936  ublbneg  9945  elq  9954  qreccl  9974  elpq  9981  ralrp  10008  rexrp  10009  rpnegap  10019  ltxr  10108  xrnemnf  10110  xrltso  10129  icc0r  10259  divelunit  10335  fzprval  10416  fztpval  10417  elfz1b  10424  fz01or  10445  4fvwrd4  10474  fzolb  10488  fzolb2  10489  elfzo3  10498  fzouzsplit  10515  elfzo0z  10523  fzo0m  10531  fzind2  10585  ioo0  10619  ico0  10621  ioc0  10622  uzennn  10798  seq3f1olemp  10877  sseqn  11203  hashfibc  11207  iswrd  11226  caucvgre  11666  cvg1nlemcau  11669  resqrexlemex  11710  climeu  11981  fsum2dlemstep  12120  expcnv  12190  prodsnf  12278  fprod2dlemstep  12308  divides  12475  m1exp1  12587  divalgb  12611  bitsval2  12630  bitsmod  12642  bitscmp  12644  bezoutlemnewy  12692  bezoutlemmain  12694  bezoutlemex  12697  dfgcd2  12710  nnwosdc  12735  lcmgcdlem  12774  isprm2  12814  isprm3  12815  isprm4  12816  isprm5  12839  sqrt2irr  12859  oddpwdc  12871  pythagtriplem19  12980  pythagtrip  12981  pceu  12993  dvdsprmpweqnn  13034  4sqlem2  13087  4sqlem12  13100  dec5dvds2  13111  ennnfoneleminc  13162  ennnfonelemex  13165  ennnfonelemr  13174  ctiunct  13191  infpn2  13207  xpsfrnel  13557  xpsfrnel2  13559  gsum0g  13609  ismnd  13632  dfgrp2e  13741  dfgrp3me  13813  isnsg2  13920  eqger  13941  isabl2  14011  imasabl  14053  isrhm  14303  isrim  14314  isnzr2  14329  lss1d  14531  istps  14897  istps2  14898  isbasis2g  14910  tgval2  14916  txuni2  15121  tx1cn  15134  tx2cn  15135  uptx  15139  txdis1cn  15143  blres  15299  xmeterval  15300  xmeter  15301  isxms2  15317  isms2  15319  metrest  15371  qtopbasss  15386  dedekindicclemicc  15497  limcdifap  15527  plyrecj  15628  pilem1  15644  sincosq1lem  15690  mpodvdsmulf1o  15858  gausslemma2dlem1a  15931  gausslemma2dlem4  15937  lgsquadlem1  15950  lgsquadlem2  15951  2lgslem1b  15962  2sqlem1  15987  upgrex  16098  griedg0ssusgr  16246  clwwlkn1loopb  16415  clwwlknon2x  16430  decidr  16568  bdcuni  16646  bdcriota  16653  bdinex1  16669  bj-zfpair2  16680  bj-axun2  16685  bj-ssom  16706  ss1oel2o  16761  nninfsellemdc  16788  nninfsellemsuc  16790  nninfsellemqall  16793  trirec0xor  16829  iswomni0  16836