Theorem bitr4i 186

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 131	. 2 |- ( ps <-> ch )
4	1, 3	bitri 183	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr2i  207  3bitr2ri  208  3bitr4i  211  3bitr4ri  212  imdistan  434  mpbiran  887  mpbiran2  888  3anrev  935  an6  1258  nfand  1506  19.33b2  1566  nf3  1605  nf4dc  1606  nf4r  1607  equsalh  1662  sb6x  1710  sb5f  1733  sbidm  1780  sb5  1816  sbanv  1818  sborv  1819  sbhb  1865  sb3an  1881  sbel2x  1923  sbal1yz  1926  sbexyz  1928  eu2  1993  2eu4  2042  cleqh  2188  cleqf  2253  dcne  2267  necon3bii  2294  ne3anior  2344  r2alf  2396  r2exf  2397  r19.23t  2480  r19.26-3  2500  r19.26m  2501  r19.43  2526  rabid2  2544  isset  2626  ralv  2637  rexv  2638  reuv  2639  rmov  2640  rexcom4b  2645  ceqsex4v  2663  ceqsex8v  2665  ceqsrexv  2748  ralrab2  2781  rexrab2  2783  reu2  2804  reu3  2806  reueq  2815  2reuswapdc  2820  reuind  2821  sbc3an  2901  rmo2ilem  2929  dfss2  3015  dfss3  3016  dfss3f  3018  ssabral  3093  rabss  3099  ssrabeq  3108  uniiunlem  3110  dfdif3  3111  ddifstab  3133  uncom  3145  inass  3211  indi  3247  difindiss  3254  difin2  3262  reupick3  3285  n0rf  3299  eq0  3305  eqv  3306  vss  3334  disj  3335  disj3  3339  undisj1  3344  undisj2  3345  exsnrex  3489  euabsn2  3515  euabsn  3516  prssg  3600  dfuni2  3661  unissb  3689  elint2  3701  ssint  3710  dfiin2g  3769  iunn0m  3796  iunxun  3815  iunxiun  3816  iinpw  3825  disjnim  3842  dftr2  3944  dftr5  3945  dftr3  3946  dftr4  3947  vnex  3976  inuni  3997  snelpw  4049  sspwb  4052  opelopabsb  4096  eusv2  4292  orddif  4376  onintexmid  4401  zfregfr  4402  tfi  4410  opthprc  4502  elxp3  4505  xpiundir  4510  elvv  4513  brinxp2  4518  relsn  4556  reliun  4571  inxp  4583  raliunxp  4590  rexiunxp  4591  cnvuni  4635  dm0rn0  4666  elrn  4691  ssdmres  4748  dfres2  4777  dfima2  4789  args  4814  cotr  4826  intasym  4829  asymref  4830  intirr  4831  cnv0  4848  xp11m  4882  cnvresima  4933  resco  4948  rnco  4950  coiun  4953  coass  4962  dfiota2  4994  dffun2  5038  dffun6f  5041  dffun4f  5044  dffun7  5055  dffun9  5057  funfn  5058  svrelfun  5092  imadiflem  5106  dffn2  5176  dffn3  5184  fintm  5209  dffn4  5252  dff1o4  5274  brprcneu  5311  eqfnfv3  5413  fnreseql  5423  fsn  5483  abrexco  5552  imaiun  5553  mpt22eqb  5768  elovmpt2  5859  abexex  5911  releldm2  5969  fnmpt2  5986  dftpos4  6042  tfrlem7  6096  0er  6340  eroveu  6397  erovlem  6398  map0e  6457  elixpconst  6477  domen  6522  reuen1  6572  xpf1o  6614  ssfilem  6645  finexdc  6672  ssfirab  6697  sbthlemi10  6729  dmaddpq  6992  dmmulpq  6993  distrnqg  7000  enq0enq  7044  enq0tr  7047  nqnq0pi  7051  distrnq0  7072  prltlu  7100  prarloc  7116  genpdflem  7120  ltexprlemm  7213  ltexprlemlol  7215  ltexprlemupu  7217  ltexprlemdisj  7219  recexprlemdisj  7243  ltresr  7430  elnnz  8814  dfz2  8873  2rexuz  9124  eluz2b1  9142  elxr  9301  elixx1  9369  elioo2  9393  elioopnf  9439  elicopnf  9441  elfz1  9483  fzdifsuc  9549  fznn  9557  fzp1nel  9572  fznn0  9581  redivap  10362  imdivap  10369  rexanre  10707  climreu  10739  3dvdsdec  11197  3dvds2dec  11198  bezoutlembi  11326  isprm2  11431  isprm3  11432  isprm4  11433  isbasis3g  11798  elcncf1di  11901  dcdc  11928  bj-vprc  12053  ss1oel2o  12154