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  1859  gencl  2792  spsbc  2997  prexg  4240  posng  4731  sosng  4732  optocl  4735  relcnvexb  5205  funimass1  5331  dmfex  5443  f1ocnvb  5514  eqfnfv2  5656  elpreima  5677  dff13  5811  f1ocnvfv  5822  f1ocnvfvb  5823  fliftfun  5839  eusvobj2  5904  mpoxopn0yelv  6292  rntpos  6310  erexb  6612  findcard2  6945  findcard2s  6946  xpfi  6986  sbthlemi3  7018  enq0tr  7494  addnqprllem  7587  addnqprulem  7588  distrlem1prl  7642  distrlem1pru  7643  recexprlem1ssl  7693  recexprlem1ssu  7694  elrealeu  7889  addcan  8199  addcan2  8200  neg11  8270  negreb  8284  mulcanapd  8680  receuap  8688  cju  8980  nn1suc  9001  nnaddcl  9002  nndivtr  9024  znegclb  9350  zaddcllempos  9354  zmulcl  9370  zeo  9422  uz11  9615  uzp1  9626  eqreznegel  9679  xneg11  9900  xnegdi  9934  modqadd1  10432  modqmul1  10448  frec2uzltd  10474  bccmpl  10825  fz1eqb  10861  eqwrd  10954  cj11  11049  rennim  11146  resqrexlemgt0  11164  efne0  11821  dvdsabseq  11989  pcfac  12488  divsfval  12911  grpinveu  13110  mulgass  13229  dvreq1  13638  unitrrg  13763  uptx  14442  hmeocnvb  14486  tgioo  14714  bj-nnbidc  15249  bj-prexg  15403  strcollnft  15476