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  1862  gencl  2795  spsbc  3001  prexg  4244  posng  4735  sosng  4736  optocl  4739  relcnvexb  5209  funimass1  5335  dmfex  5447  f1ocnvb  5518  eqfnfv2  5660  elpreima  5681  dff13  5815  f1ocnvfv  5826  f1ocnvfvb  5827  fliftfun  5843  eusvobj2  5908  mpoxopn0yelv  6297  rntpos  6315  erexb  6617  findcard2  6950  findcard2s  6951  xpfi  6993  sbthlemi3  7025  enq0tr  7501  addnqprllem  7594  addnqprulem  7595  distrlem1prl  7649  distrlem1pru  7650  recexprlem1ssl  7700  recexprlem1ssu  7701  elrealeu  7896  addcan  8206  addcan2  8207  neg11  8277  negreb  8291  mulcanapd  8688  receuap  8696  cju  8988  nn1suc  9009  nnaddcl  9010  nndivtr  9032  znegclb  9359  zaddcllempos  9363  zmulcl  9379  zeo  9431  uz11  9624  uzp1  9635  eqreznegel  9688  xneg11  9909  xnegdi  9943  modqadd1  10453  modqmul1  10469  frec2uzltd  10495  bccmpl  10846  fz1eqb  10882  eqwrd  10975  cj11  11070  rennim  11167  resqrexlemgt0  11185  efne0  11843  dvdsabseq  12012  pcfac  12519  divsfval  12971  grpinveu  13170  mulgass  13289  dvreq1  13698  unitrrg  13823  uptx  14510  hmeocnvb  14554  tgioo  14790  bj-nnbidc  15403  bj-prexg  15557  strcollnft  15630