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  4305  eusv2  4503  orddif  4594  onintexmid  4620  zfregfr  4621  tfi  4629  opthprc  4725  elxp3  4728  xpiundir  4733  elvv  4736  brinxp2  4741  relsn  4779  reliun  4795  inxp  4811  raliunxp  4818  rexiunxp  4819  cnvuni  4863  dm0rn0  4894  elrn  4920  ssdmres  4980  dfres2  5010  dfima2  5023  args  5050  cotr  5063  intasym  5066  asymref  5067  intirr  5068  cnv0  5085  xp11m  5120  cnvresima  5171  resco  5186  rnco  5188  coiun  5191  coass  5200  dfiota2  5232  dffun2  5280  dffun6f  5283  dffun4f  5286  dffun7  5297  dffun9  5299  funfn  5300  svrelfun  5338  imadiflem  5352  dffn2  5426  dffn3  5435  fintm  5460  dffn4  5503  dff1o4  5529  brprcneu  5568  eqfnfv3  5678  fnreseql  5689  fsn  5751  abrexco  5827  imaiun  5828  mpo2eqb  6054  elovmpo  6144  abexex  6210  releldm2  6270  fnmpo  6287  dftpos4  6348  tfrlem7  6402  0er  6653  eroveu  6712  erovlem  6713  map0e  6772  elixpconst  6792  domen  6839  reuen1  6892  xpf1o  6940  ssfilem  6971  finexdc  6998  pw1dc0el  7007  ssfirab  7032  sbthlemi10  7067  djuexb  7145  dmaddpq  7491  dmmulpq  7492  distrnqg  7499  enq0enq  7543  enq0tr  7546  nqnq0pi  7550  distrnq0  7571  prltlu  7599  prarloc  7615  genpdflem  7619  ltexprlemm  7712  ltexprlemlol  7714  ltexprlemupu  7716  ltexprlemdisj  7718  recexprlemdisj  7742  ltresr  7951  elnnz  9381  dfz2  9444  2rexuz  9702  eluz2b1  9721  elxr  9897  elixx1  10018  elioo2  10042  elioopnf  10088  elicopnf  10090  elfz1  10134  fzdifsuc  10202  fznn  10210  fzp1nel  10225  fznn0  10234  dfrp2  10404  redivap  11127  imdivap  11134  rexanre  11473  climreu  11550  prodmodc  11831  3dvdsdec  12118  3dvds2dec  12119  bitsval  12196  bezoutlembi  12268  nnwosdc  12302  isprm2  12381  isprm3  12382  isprm4  12383  pythagtriplem2  12531  elgz  12636  inffinp1  12742  isnsg4  13490  isrng  13638  isring  13704  dfrhm2  13858  lss1d  14087  isbasis3g  14460  restsn  14594  lmbr  14627  txbas  14672  tx2cn  14684  elcncf1di  14993  dedekindicclemicc  15046  limcrcl  15072  bj-nnor  15603  bj-vprc  15765  ss1oel2o  15861  subctctexmid  15870  trirec0xor  15917