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  614  mpbiran  946  mpbiran2  947  3anrev  1012  an6  1355  nfand  1614  19.33b2  1675  nf3  1715  nf4dc  1716  nf4r  1717  equsalh  1772  sb6x  1825  sb5f  1850  sbidm  1897  sb5  1934  sbanv  1936  sborv  1937  sbhb  1991  sb3an  2009  sbel2x  2049  sbal1yz  2052  sbexyz  2054  eu2  2122  2eu4  2171  cleqh  2329  cleqf  2397  dcne  2411  necon3bii  2438  ne3anior  2488  r2alf  2547  r2exf  2548  r19.23t  2638  r19.26-3  2661  r19.26m  2662  r19.43  2689  rabid2  2708  isset  2807  ralv  2818  rexv  2819  reuv  2820  rmov  2821  rexcom4b  2826  ceqsex4v  2845  ceqsex8v  2847  ceqsrexv  2934  ralrab2  2969  rexrab2  2971  reu2  2992  reu3  2994  reueq  3003  2reuswapdc  3008  reuind  3009  sbc3an  3091  rmo2ilem  3120  csbcow  3136  ssalel  3213  dfss3  3214  dfss3f  3217  ssabral  3296  rabss  3302  ssrabeq  3312  uniiunlem  3314  dfdif3  3315  ddifstab  3337  uncom  3349  inass  3415  indi  3452  difindiss  3459  difin2  3467  reupick3  3490  n0rf  3505  eq0  3511  eqv  3512  vss  3540  disj  3541  disj3  3545  undisj1  3550  undisj2  3551  exsnrex  3709  euabsn2  3738  euabsn  3739  snmb  3791  prssg  3828  dfuni2  3893  unissb  3921  elint2  3933  ssint  3942  dfiin2g  4001  iunn0m  4029  iunxun  4048  iunxiun  4050  iinpw  4059  disjnim  4076  dftr2  4187  dftr5  4188  dftr3  4189  dftr4  4190  vnex  4218  inuni  4243  snelpw  4302  sspwb  4306  opelopabsb  4352  eusv2  4552  orddif  4643  onintexmid  4669  zfregfr  4670  tfi  4678  opthprc  4775  elxp3  4778  xpiundir  4783  elvv  4786  brinxp2  4791  relsn  4829  reliun  4846  inxp  4862  raliunxp  4869  rexiunxp  4870  cnvuni  4914  dm0rn0  4946  elrn  4973  ssdmres  5033  dfres2  5063  dfima2  5076  args  5103  cotr  5116  intasym  5119  asymref  5120  intirr  5121  cnv0  5138  xp11m  5173  cnvresima  5224  resco  5239  rnco  5241  coiun  5244  coass  5253  dfiota2  5285  dffun2  5334  dffun6f  5337  dffun4f  5340  dffun7  5351  dffun9  5353  funfn  5354  svrelfun  5392  imadiflem  5406  dffn2  5481  dffn3  5490  fintm  5519  dffn4  5562  dff1o4  5588  brprcneu  5628  eqfnfv3  5742  fnreseql  5753  fsn  5815  abrexco  5895  imaiun  5896  mpo2eqb  6126  elovmpo  6216  abexex  6283  releldm2  6343  fnmpo  6362  dftpos4  6424  tfrlem7  6478  0er  6731  eroveu  6790  erovlem  6791  map0e  6850  elixpconst  6870  domen  6917  reuen1  6970  xpf1o  7025  ssfilem  7057  finexdc  7085  pw1dc0el  7096  ssfirab  7121  sbthlemi10  7156  djuexb  7234  iftrueb01  7431  pw1if  7433  dmaddpq  7589  dmmulpq  7590  distrnqg  7597  enq0enq  7641  enq0tr  7644  nqnq0pi  7648  distrnq0  7669  prltlu  7697  prarloc  7713  genpdflem  7717  ltexprlemm  7810  ltexprlemlol  7812  ltexprlemupu  7814  ltexprlemdisj  7816  recexprlemdisj  7840  ltresr  8049  elnnz  9479  dfz2  9542  2rexuz  9806  eluz2b1  9825  elxr  10001  elixx1  10122  elioo2  10146  elioopnf  10192  elicopnf  10194  elfz1  10238  fzdifsuc  10306  fznn  10314  fzp1nel  10329  fznn0  10338  dfrp2  10513  redivap  11425  imdivap  11432  rexanre  11771  climreu  11848  prodmodc  12129  3dvdsdec  12416  3dvds2dec  12417  bitsval  12494  bezoutlembi  12566  nnwosdc  12600  isprm2  12679  isprm3  12680  isprm4  12681  pythagtriplem2  12829  elgz  12934  inffinp1  13040  isnsg4  13789  isrng  13937  isring  14003  dfrhm2  14158  lss1d  14387  isbasis3g  14760  restsn  14894  lmbr  14927  txbas  14972  tx2cn  14984  elcncf1di  15293  dedekindicclemicc  15346  limcrcl  15372  isclwwlk  16189  clwwlkccatlem  16195  bj-nnor  16266  bj-vprc  16427  ss1oel2o  16522  subctctexmid  16537  trirec0xor  16585