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  5617  fnreseql  5628  fsn  5690  abrexco  5762  imaiun  5763  mpo2eqb  5986  elovmpo  6074  abexex  6129  releldm2  6188  fnmpo  6205  dftpos4  6266  tfrlem7  6320  0er  6571  eroveu  6628  erovlem  6629  map0e  6688  elixpconst  6708  domen  6753  reuen1  6803  xpf1o  6846  ssfilem  6877  finexdc  6904  pw1dc0el  6913  ssfirab  6935  sbthlemi10  6967  djuexb  7045  dmaddpq  7380  dmmulpq  7381  distrnqg  7388  enq0enq  7432  enq0tr  7435  nqnq0pi  7439  distrnq0  7460  prltlu  7488  prarloc  7504  genpdflem  7508  ltexprlemm  7601  ltexprlemlol  7603  ltexprlemupu  7605  ltexprlemdisj  7607  recexprlemdisj  7631  ltresr  7840  elnnz  9265  dfz2  9327  2rexuz  9584  eluz2b1  9603  elxr  9778  elixx1  9899  elioo2  9923  elioopnf  9969  elicopnf  9971  elfz1  10015  fzdifsuc  10083  fznn  10091  fzp1nel  10106  fznn0  10115  dfrp2  10266  redivap  10885  imdivap  10892  rexanre  11231  climreu  11307  prodmodc  11588  3dvdsdec  11872  3dvds2dec  11873  bezoutlembi  12008  nnwosdc  12042  isprm2  12119  isprm3  12120  isprm4  12121  pythagtriplem2  12268  elgz  12371  inffinp1  12432  isnsg4  13077  isring  13188  lss1d  13475  isbasis3g  13631  restsn  13765  lmbr  13798  txbas  13843  tx2cn  13855  elcncf1di  14151  dedekindicclemicc  14195  limcrcl  14212  bj-nnor  14571  bj-vprc  14733  ss1oel2o  14828  subctctexmid  14835  trirec0xor  14878