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  612  mpbiran  940  mpbiran2  941  3anrev  988  an6  1321  nfand  1568  19.33b2  1629  nf3  1669  nf4dc  1670  nf4r  1671  equsalh  1726  sb6x  1779  sb5f  1804  sbidm  1851  sb5  1887  sbanv  1889  sborv  1890  sbhb  1940  sb3an  1958  sbel2x  1998  sbal1yz  2001  sbexyz  2003  eu2  2070  2eu4  2119  cleqh  2277  cleqf  2344  dcne  2358  necon3bii  2385  ne3anior  2435  r2alf  2494  r2exf  2495  r19.23t  2584  r19.26-3  2607  r19.26m  2608  r19.43  2635  rabid2  2654  isset  2745  ralv  2756  rexv  2757  reuv  2758  rmov  2759  rexcom4b  2764  ceqsex4v  2782  ceqsex8v  2784  ceqsrexv  2869  ralrab2  2904  rexrab2  2906  reu2  2927  reu3  2929  reueq  2938  2reuswapdc  2943  reuind  2944  sbc3an  3026  rmo2ilem  3054  csbcow  3070  dfss2  3146  dfss3  3147  dfss3f  3149  ssabral  3228  rabss  3234  ssrabeq  3244  uniiunlem  3246  dfdif3  3247  ddifstab  3269  uncom  3281  inass  3347  indi  3384  difindiss  3391  difin2  3399  reupick3  3422  n0rf  3437  eq0  3443  eqv  3444  vss  3472  disj  3473  disj3  3477  undisj1  3482  undisj2  3483  exsnrex  3636  euabsn2  3663  euabsn  3664  prssg  3751  dfuni2  3813  unissb  3841  elint2  3853  ssint  3862  dfiin2g  3921  iunn0m  3949  iunxun  3968  iunxiun  3970  iinpw  3979  disjnim  3996  dftr2  4105  dftr5  4106  dftr3  4107  dftr4  4108  vnex  4136  inuni  4157  snelpw  4215  sspwb  4218  opelopabsb  4262  eusv2  4459  orddif  4548  onintexmid  4574  zfregfr  4575  tfi  4583  opthprc  4679  elxp3  4682  xpiundir  4687  elvv  4690  brinxp2  4695  relsn  4733  reliun  4749  inxp  4763  raliunxp  4770  rexiunxp  4771  cnvuni  4815  dm0rn0  4846  elrn  4872  ssdmres  4931  dfres2  4961  dfima2  4974  args  4999  cotr  5012  intasym  5015  asymref  5016  intirr  5017  cnv0  5034  xp11m  5069  cnvresima  5120  resco  5135  rnco  5137  coiun  5140  coass  5149  dfiota2  5181  dffun2  5228  dffun6f  5231  dffun4f  5234  dffun7  5245  dffun9  5247  funfn  5248  svrelfun  5283  imadiflem  5297  dffn2  5369  dffn3  5378  fintm  5403  dffn4  5446  dff1o4  5471  brprcneu  5510  eqfnfv3  5618  fnreseql  5629  fsn  5691  abrexco  5763  imaiun  5764  mpo2eqb  5987  elovmpo  6075  abexex  6130  releldm2  6189  fnmpo  6206  dftpos4  6267  tfrlem7  6321  0er  6572  eroveu  6629  erovlem  6630  map0e  6689  elixpconst  6709  domen  6754  reuen1  6804  xpf1o  6847  ssfilem  6878  finexdc  6905  pw1dc0el  6914  ssfirab  6936  sbthlemi10  6968  djuexb  7046  dmaddpq  7381  dmmulpq  7382  distrnqg  7389  enq0enq  7433  enq0tr  7436  nqnq0pi  7440  distrnq0  7461  prltlu  7489  prarloc  7505  genpdflem  7509  ltexprlemm  7602  ltexprlemlol  7604  ltexprlemupu  7606  ltexprlemdisj  7608  recexprlemdisj  7632  ltresr  7841  elnnz  9266  dfz2  9328  2rexuz  9585  eluz2b1  9604  elxr  9779  elixx1  9900  elioo2  9924  elioopnf  9970  elicopnf  9972  elfz1  10016  fzdifsuc  10084  fznn  10092  fzp1nel  10107  fznn0  10116  dfrp2  10267  redivap  10886  imdivap  10893  rexanre  11232  climreu  11308  prodmodc  11589  3dvdsdec  11873  3dvds2dec  11874  bezoutlembi  12009  nnwosdc  12043  isprm2  12120  isprm3  12121  isprm4  12122  pythagtriplem2  12269  elgz  12372  inffinp1  12433  isnsg4  13078  isring  13189  lss1d  13476  isbasis3g  13686  restsn  13820  lmbr  13853  txbas  13898  tx2cn  13910  elcncf1di  14206  dedekindicclemicc  14250  limcrcl  14267  bj-nnor  14626  bj-vprc  14788  ss1oel2o  14884  subctctexmid  14891  trirec0xor  14934