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  942  mpbiran2  943  3anrev  990  an6  1333  nfand  1590  19.33b2  1651  nf3  1691  nf4dc  1692  nf4r  1693  equsalh  1748  sb6x  1801  sb5f  1826  sbidm  1873  sb5  1910  sbanv  1912  sborv  1913  sbhb  1967  sb3an  1985  sbel2x  2025  sbal1yz  2028  sbexyz  2030  eu2  2097  2eu4  2146  cleqh  2304  cleqf  2372  dcne  2386  necon3bii  2413  ne3anior  2463  r2alf  2522  r2exf  2523  r19.23t  2612  r19.26-3  2635  r19.26m  2636  r19.43  2663  rabid2  2682  isset  2777  ralv  2788  rexv  2789  reuv  2790  rmov  2791  rexcom4b  2796  ceqsex4v  2815  ceqsex8v  2817  ceqsrexv  2902  ralrab2  2937  rexrab2  2939  reu2  2960  reu3  2962  reueq  2971  2reuswapdc  2976  reuind  2977  sbc3an  3059  rmo2ilem  3087  csbcow  3103  ssalel  3180  dfss3  3181  dfss3f  3184  ssabral  3263  rabss  3269  ssrabeq  3279  uniiunlem  3281  dfdif3  3282  ddifstab  3304  uncom  3316  inass  3382  indi  3419  difindiss  3426  difin2  3434  reupick3  3457  n0rf  3472  eq0  3478  eqv  3479  vss  3507  disj  3508  disj3  3512  undisj1  3517  undisj2  3518  exsnrex  3674  euabsn2  3701  euabsn  3702  prssg  3789  dfuni2  3851  unissb  3879  elint2  3891  ssint  3900  dfiin2g  3959  iunn0m  3987  iunxun  4006  iunxiun  4008  iinpw  4017  disjnim  4034  dftr2  4143  dftr5  4144  dftr3  4145  dftr4  4146  vnex  4174  inuni  4198  snelpw  4256  sspwb  4259  opelopabsb  4304  eusv2  4502  orddif  4593  onintexmid  4619  zfregfr  4620  tfi  4628  opthprc  4724  elxp3  4727  xpiundir  4732  elvv  4735  brinxp2  4740  relsn  4778  reliun  4794  inxp  4810  raliunxp  4817  rexiunxp  4818  cnvuni  4862  dm0rn0  4893  elrn  4919  ssdmres  4978  dfres2  5008  dfima2  5021  args  5048  cotr  5061  intasym  5064  asymref  5065  intirr  5066  cnv0  5083  xp11m  5118  cnvresima  5169  resco  5184  rnco  5186  coiun  5189  coass  5198  dfiota2  5230  dffun2  5278  dffun6f  5281  dffun4f  5284  dffun7  5295  dffun9  5297  funfn  5298  svrelfun  5333  imadiflem  5347  dffn2  5421  dffn3  5430  fintm  5455  dffn4  5498  dff1o4  5524  brprcneu  5563  eqfnfv3  5673  fnreseql  5684  fsn  5746  abrexco  5818  imaiun  5819  mpo2eqb  6045  elovmpo  6135  abexex  6201  releldm2  6261  fnmpo  6278  dftpos4  6339  tfrlem7  6393  0er  6644  eroveu  6703  erovlem  6704  map0e  6763  elixpconst  6783  domen  6828  reuen1  6878  xpf1o  6923  ssfilem  6954  finexdc  6981  pw1dc0el  6990  ssfirab  7015  sbthlemi10  7050  djuexb  7128  dmaddpq  7474  dmmulpq  7475  distrnqg  7482  enq0enq  7526  enq0tr  7529  nqnq0pi  7533  distrnq0  7554  prltlu  7582  prarloc  7598  genpdflem  7602  ltexprlemm  7695  ltexprlemlol  7697  ltexprlemupu  7699  ltexprlemdisj  7701  recexprlemdisj  7725  ltresr  7934  elnnz  9364  dfz2  9427  2rexuz  9685  eluz2b1  9704  elxr  9880  elixx1  10001  elioo2  10025  elioopnf  10071  elicopnf  10073  elfz1  10117  fzdifsuc  10185  fznn  10193  fzp1nel  10208  fznn0  10217  dfrp2  10387  redivap  11104  imdivap  11111  rexanre  11450  climreu  11527  prodmodc  11808  3dvdsdec  12095  3dvds2dec  12096  bitsval  12173  bezoutlembi  12245  nnwosdc  12279  isprm2  12358  isprm3  12359  isprm4  12360  pythagtriplem2  12508  elgz  12613  inffinp1  12719  isnsg4  13466  isrng  13614  isring  13680  dfrhm2  13834  lss1d  14063  isbasis3g  14436  restsn  14570  lmbr  14603  txbas  14648  tx2cn  14660  elcncf1di  14969  dedekindicclemicc  15022  limcrcl  15048  bj-nnor  15534  bj-vprc  15696  ss1oel2o  15792  subctctexmid  15801  trirec0xor  15848