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  1848  gencl  2769  spsbc  2974  prexg  4211  posng  4698  sosng  4699  optocl  4702  relcnvexb  5168  funimass1  5293  dmfex  5405  f1ocnvb  5475  eqfnfv2  5614  elpreima  5635  dff13  5768  f1ocnvfv  5779  f1ocnvfvb  5780  fliftfun  5796  eusvobj2  5860  mpoxopn0yelv  6239  rntpos  6257  erexb  6559  findcard2  6888  findcard2s  6889  xpfi  6928  sbthlemi3  6957  enq0tr  7432  addnqprllem  7525  addnqprulem  7526  distrlem1prl  7580  distrlem1pru  7581  recexprlem1ssl  7631  recexprlem1ssu  7632  elrealeu  7827  addcan  8135  addcan2  8136  neg11  8206  negreb  8220  mulcanapd  8616  receuap  8624  cju  8916  nn1suc  8936  nnaddcl  8937  nndivtr  8959  znegclb  9284  zaddcllempos  9288  zmulcl  9304  zeo  9356  uz11  9548  uzp1  9559  eqreznegel  9612  xneg11  9832  xnegdi  9866  modqadd1  10358  modqmul1  10374  frec2uzltd  10400  bccmpl  10729  fz1eqb  10765  cj11  10909  rennim  11006  resqrexlemgt0  11024  efne0  11681  dvdsabseq  11847  pcfac  12342  grpinveu  12865  mulgass  12973  dvreq1  13264  uptx  13667  hmeocnvb  13711  tgioo  13939  bj-nnbidc  14391  bj-prexg  14545  strcollnft  14618