Theorem bitr4i 187

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr4i.1	|- ( ph <-> ps )
bitr4i.2	|- ( ch <-> ps )

Assertion

Ref	Expression
bitr4i	|- ( ph <-> ch )

Proof of Theorem bitr4i

Step	Hyp	Ref	Expression
1		bitr4i.1	. 2 |- ( ph <-> ps )
2		bitr4i.2	. . 3 |- ( ch <-> ps )
3	2	bicomi 132	. 2 |- ( ps <-> ch )
4	1, 3	bitri 184	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:  3bitr2i  208  3bitr2ri  209  3bitr4i  212  3bitr4ri  213  biancomi  270  imdistan  444  bianass  469  biadani  616  mpbiran  949  mpbiran2  950  3anrev  1015  an6  1358  nfand  1617  19.33b2  1678  nf3  1717  nf4dc  1718  nf4r  1719  equsalh  1774  sb6x  1828  sb5f  1853  sbidm  1900  equsv  1934  sb5  1938  sbanv  1940  sborv  1941  sbhb  1996  sb3an  2014  sbel2x  2054  sbal1yz  2057  sbexyz  2059  eu2  2127  2eu4  2176  cleqh  2334  cleqf  2411  dcne  2425  necon3bii  2452  ne3anior  2502  r2alf  2561  r2exf  2562  r19.23t  2652  r19.26-3  2675  r19.26m  2676  r19.43  2703  rabid2  2723  isset  2822  ralv  2833  rexv  2834  reuv  2835  rmov  2836  rexcom4b  2841  ceqsex4v  2860  ceqsex8v  2862  ceqsrexv  2950  ralrab2  2985  rexrab2  2987  reu2  3008  reu3  3010  reueq  3019  2reuswapdc  3024  reuind  3025  sbc3an  3107  rmo2ilem  3136  csbcow  3152  ssalel  3229  dfss3  3230  dfss3f  3234  ssabral  3313  rabss  3319  ssrabeq  3330  uniiunlem  3332  dfdif3  3333  ddifstab  3355  uncom  3367  inass  3435  indi  3472  difindiss  3479  difin2  3487  reupick3  3510  n0rf  3525  eq0  3531  eqv  3532  vss  3560  disj  3561  disj3  3565  undisj1  3570  undisj2  3571  exsnrex  3736  euabsn2  3765  euabsn  3766  snmb  3818  prssg  3856  dfuni2  3921  unissb  3949  elint2  3961  ssint  3970  dfiin2g  4029  iunn0m  4057  iunxun  4076  iunxiun  4078  iinpw  4087  disjnim  4104  dftr2  4215  dftr5  4216  dftr3  4217  dftr4  4218  vnex  4246  inuni  4272  snelpw  4333  sspwb  4337  opelopabsb  4383  eusv2  4583  orddif  4674  onintexmid  4700  zfregfr  4701  tfi  4709  opthprc  4806  elxp3  4809  xpiundir  4814  elvv  4817  brinxp2  4822  relsn  4860  reliun  4878  inxp  4894  raliunxp  4901  rexiunxp  4902  cnvuni  4946  dm0rn0  4978  elrn  5005  ssdmres  5065  dfres2  5095  dfima2  5108  args  5136  cotr  5149  intasym  5152  asymref  5153  intirr  5154  cnv0  5171  xp11m  5206  cnvresima  5257  resco  5272  rnco  5274  coiun  5277  coass  5286  dfiota2  5318  dffun2  5367  dffun6f  5370  dffun4f  5373  dffun7  5384  dffun9  5386  funfn  5387  svrelfun  5426  imadiflem  5440  dffn2  5515  dffn3  5524  fintm  5557  dffn4  5601  dff1o4  5627  brprcneu  5668  eqfnfv3  5782  fnreseql  5793  fsn  5854  abrexco  5938  imaiun  5939  mpo2eqb  6171  elovmpo  6261  abexex  6328  releldm2  6392  fnmpo  6411  cnvimadfsn  6458  dftpos4  6507  tfrlem7  6561  0er  6814  eroveu  6873  erovlem  6874  map0e  6933  elixpconst  6954  domen  7001  reuen1  7054  xpf1o  7110  ssfilem  7143  ssfilemd  7145  finexdc  7173  pw1dc0el  7184  ssfirab  7210  sbthlemi10  7249  djuexb  7348  sspw1or2  7508  iftrueb01  7546  pw1if  7548  dmaddpq  7710  dmmulpq  7711  distrnqg  7718  enq0enq  7762  enq0tr  7765  nqnq0pi  7769  distrnq0  7790  prltlu  7818  prarloc  7834  genpdflem  7838  ltexprlemm  7931  ltexprlemlol  7933  ltexprlemupu  7935  ltexprlemdisj  7937  recexprlemdisj  7961  ltresr  8170  elnnz  9604  dfz2  9667  2rexuz  9932  eluz2b1  9951  elxr  10128  elixx1  10249  elioo2  10273  elioopnf  10319  elicopnf  10321  elfz1  10366  fzdifsuc  10437  fznn  10445  fzp1nel  10460  fznn0  10469  dfrp2  10647  redivap  11584  imdivap  11591  rexanre  11930  climreu  12007  prodmodc  12289  3dvdsdec  12576  3dvds2dec  12577  bitsval  12654  bezoutlembi  12726  nnwosdc  12760  isprm2  12839  isprm3  12840  isprm4  12841  pythagtriplem2  12989  elgz  13094  inffinp1  13264  isnsg4  13965  isrng  14173  isring  14243  dfrhm2  14399  lss1d  14657  isbasis3g  15037  restsn  15171  lmbr  15204  txbas  15249  tx2cn  15261  elcncf1di  15570  dedekindicclemicc  15623  limcrcl  15649  isclwwlk  16515  clwwlkccatlem  16521  eupth2lem1  16579  bj-nnor  16632  bj-vprc  16792  ss1oel2o  16887  subctctexmid  16900  trirec0xor  16955