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  1896  gencl  2835  spsbc  3043  prexg  4301  posng  4798  sosng  4799  optocl  4802  relcnvexb  5276  funimass1  5407  dmfex  5526  f1ocnvb  5597  eqfnfv2  5745  elpreima  5766  dff13  5908  f1ocnvfv  5919  f1ocnvfvb  5920  fliftfun  5936  eusvobj2  6003  mpoxopn0yelv  6404  rntpos  6422  erexb  6726  findcard2  7077  findcard2s  7078  xpfi  7123  sbthlemi3  7157  enq0tr  7653  addnqprllem  7746  addnqprulem  7747  distrlem1prl  7801  distrlem1pru  7802  recexprlem1ssl  7852  recexprlem1ssu  7853  elrealeu  8048  addcan  8358  addcan2  8359  neg11  8429  negreb  8443  mulcanapd  8840  receuap  8848  cju  9140  nn1suc  9161  nnaddcl  9162  nndivtr  9184  znegclb  9511  zaddcllempos  9515  zmulcl  9532  zeo  9584  uz11  9778  uzp1  9789  eqreznegel  9847  xneg11  10068  xnegdi  10102  modqadd1  10622  modqmul1  10638  frec2uzltd  10664  bccmpl  11015  fz1eqb  11051  eqwrd  11153  ccatopth  11296  ccatopth2  11297  swrdccatin2  11309  cj11  11465  rennim  11562  resqrexlemgt0  11580  efne0  12238  dvdsabseq  12407  pcfac  12922  divsfval  13410  grpinveu  13620  mulgass  13745  dvreq1  14155  unitrrg  14280  uptx  14997  hmeocnvb  15041  tgioo  15277  uspgrf1oedg  16026  usgr0vb  16083  bj-nnbidc  16353  bj-prexg  16506  strcollnft  16579