Theorem imbitrid 154

Description: A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.)

Hypotheses

Ref	Expression
imbitrid.1	|- ( ph -> ps )
imbitrid.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
imbitrid	|- ( ch -> ( ph -> th ) )

Proof of Theorem imbitrid

Step	Hyp	Ref	Expression
1		imbitrid.1	. 2 |- ( ph -> ps )
2		imbitrid.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	2	biimpd 144	. 2 |- ( ch -> ( ps -> th ) )
4	1, 3	syl5 32	1 |- ( ch -> ( ph -> th ) )

Syntax hints:   -> wi 4   <-> wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl5ibcom  155  imbitrrid  156  sbft  1872  gencl  2806  spsbc  3014  prexg  4263  posng  4755  sosng  4756  optocl  4759  relcnvexb  5231  funimass1  5360  dmfex  5477  f1ocnvb  5548  eqfnfv2  5691  elpreima  5712  dff13  5850  f1ocnvfv  5861  f1ocnvfvb  5862  fliftfun  5878  eusvobj2  5943  mpoxopn0yelv  6338  rntpos  6356  erexb  6658  findcard2  7001  findcard2s  7002  xpfi  7044  sbthlemi3  7076  enq0tr  7567  addnqprllem  7660  addnqprulem  7661  distrlem1prl  7715  distrlem1pru  7716  recexprlem1ssl  7766  recexprlem1ssu  7767  elrealeu  7962  addcan  8272  addcan2  8273  neg11  8343  negreb  8357  mulcanapd  8754  receuap  8762  cju  9054  nn1suc  9075  nnaddcl  9076  nndivtr  9098  znegclb  9425  zaddcllempos  9429  zmulcl  9446  zeo  9498  uz11  9691  uzp1  9702  eqreznegel  9755  xneg11  9976  xnegdi  10010  modqadd1  10528  modqmul1  10544  frec2uzltd  10570  bccmpl  10921  fz1eqb  10957  eqwrd  11056  ccatopth  11192  ccatopth2  11193  cj11  11291  rennim  11388  resqrexlemgt0  11406  efne0  12064  dvdsabseq  12233  pcfac  12748  divsfval  13235  grpinveu  13445  mulgass  13570  dvreq1  13979  unitrrg  14104  uptx  14821  hmeocnvb  14865  tgioo  15101  bj-nnbidc  15832  bj-prexg  15985  strcollnft  16058