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  1332  nfand  1582  19.33b2  1643  nf3  1683  nf4dc  1684  nf4r  1685  equsalh  1740  sb6x  1793  sb5f  1818  sbidm  1865  sb5  1902  sbanv  1904  sborv  1905  sbhb  1959  sb3an  1977  sbel2x  2017  sbal1yz  2020  sbexyz  2022  eu2  2089  2eu4  2138  cleqh  2296  cleqf  2364  dcne  2378  necon3bii  2405  ne3anior  2455  r2alf  2514  r2exf  2515  r19.23t  2604  r19.26-3  2627  r19.26m  2628  r19.43  2655  rabid2  2674  isset  2769  ralv  2780  rexv  2781  reuv  2782  rmov  2783  rexcom4b  2788  ceqsex4v  2807  ceqsex8v  2809  ceqsrexv  2894  ralrab2  2929  rexrab2  2931  reu2  2952  reu3  2954  reueq  2963  2reuswapdc  2968  reuind  2969  sbc3an  3051  rmo2ilem  3079  csbcow  3095  ssalel  3172  dfss3  3173  dfss3f  3176  ssabral  3255  rabss  3261  ssrabeq  3271  uniiunlem  3273  dfdif3  3274  ddifstab  3296  uncom  3308  inass  3374  indi  3411  difindiss  3418  difin2  3426  reupick3  3449  n0rf  3464  eq0  3470  eqv  3471  vss  3499  disj  3500  disj3  3504  undisj1  3509  undisj2  3510  exsnrex  3665  euabsn2  3692  euabsn  3693  prssg  3780  dfuni2  3842  unissb  3870  elint2  3882  ssint  3891  dfiin2g  3950  iunn0m  3978  iunxun  3997  iunxiun  3999  iinpw  4008  disjnim  4025  dftr2  4134  dftr5  4135  dftr3  4136  dftr4  4137  vnex  4165  inuni  4189  snelpw  4247  sspwb  4250  opelopabsb  4295  eusv2  4493  orddif  4584  onintexmid  4610  zfregfr  4611  tfi  4619  opthprc  4715  elxp3  4718  xpiundir  4723  elvv  4726  brinxp2  4731  relsn  4769  reliun  4785  inxp  4801  raliunxp  4808  rexiunxp  4809  cnvuni  4853  dm0rn0  4884  elrn  4910  ssdmres  4969  dfres2  4999  dfima2  5012  args  5039  cotr  5052  intasym  5055  asymref  5056  intirr  5057  cnv0  5074  xp11m  5109  cnvresima  5160  resco  5175  rnco  5177  coiun  5180  coass  5189  dfiota2  5221  dffun2  5269  dffun6f  5272  dffun4f  5275  dffun7  5286  dffun9  5288  funfn  5289  svrelfun  5324  imadiflem  5338  dffn2  5412  dffn3  5421  fintm  5446  dffn4  5489  dff1o4  5515  brprcneu  5554  eqfnfv3  5664  fnreseql  5675  fsn  5737  abrexco  5809  imaiun  5810  mpo2eqb  6036  elovmpo  6126  abexex  6192  releldm2  6252  fnmpo  6269  dftpos4  6330  tfrlem7  6384  0er  6635  eroveu  6694  erovlem  6695  map0e  6754  elixpconst  6774  domen  6819  reuen1  6869  xpf1o  6914  ssfilem  6945  finexdc  6972  pw1dc0el  6981  ssfirab  7006  sbthlemi10  7041  djuexb  7119  dmaddpq  7463  dmmulpq  7464  distrnqg  7471  enq0enq  7515  enq0tr  7518  nqnq0pi  7522  distrnq0  7543  prltlu  7571  prarloc  7587  genpdflem  7591  ltexprlemm  7684  ltexprlemlol  7686  ltexprlemupu  7688  ltexprlemdisj  7690  recexprlemdisj  7714  ltresr  7923  elnnz  9353  dfz2  9415  2rexuz  9673  eluz2b1  9692  elxr  9868  elixx1  9989  elioo2  10013  elioopnf  10059  elicopnf  10061  elfz1  10105  fzdifsuc  10173  fznn  10181  fzp1nel  10196  fznn0  10205  dfrp2  10370  redivap  11056  imdivap  11063  rexanre  11402  climreu  11479  prodmodc  11760  3dvdsdec  12047  3dvds2dec  12048  bitsval  12125  bezoutlembi  12197  nnwosdc  12231  isprm2  12310  isprm3  12311  isprm4  12312  pythagtriplem2  12460  elgz  12565  inffinp1  12671  isnsg4  13418  isrng  13566  isring  13632  dfrhm2  13786  lss1d  14015  isbasis3g  14366  restsn  14500  lmbr  14533  txbas  14578  tx2cn  14590  elcncf1di  14899  dedekindicclemicc  14952  limcrcl  14978  bj-nnor  15464  bj-vprc  15626  ss1oel2o  15722  subctctexmid  15731  trirec0xor  15776