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  5909  f1ocnvfv  5920  f1ocnvfvb  5921  fliftfun  5937  eusvobj2  6004  mpoxopn0yelv  6405  rntpos  6423  erexb  6727  findcard2  7078  findcard2s  7079  xpfi  7124  sbthlemi3  7158  enq0tr  7654  addnqprllem  7747  addnqprulem  7748  distrlem1prl  7802  distrlem1pru  7803  recexprlem1ssl  7853  recexprlem1ssu  7854  elrealeu  8049  addcan  8359  addcan2  8360  neg11  8430  negreb  8444  mulcanapd  8841  receuap  8849  cju  9141  nn1suc  9162  nnaddcl  9163  nndivtr  9185  znegclb  9512  zaddcllempos  9516  zmulcl  9533  zeo  9585  uz11  9779  uzp1  9790  eqreznegel  9848  xneg11  10069  xnegdi  10103  modqadd1  10624  modqmul1  10640  frec2uzltd  10666  bccmpl  11017  fz1eqb  11053  eqwrd  11158  ccatopth  11301  ccatopth2  11302  swrdccatin2  11314  cj11  11483  rennim  11580  resqrexlemgt0  11598  efne0  12257  dvdsabseq  12426  pcfac  12941  divsfval  13429  grpinveu  13639  mulgass  13764  dvreq1  14175  unitrrg  14300  uptx  15017  hmeocnvb  15061  tgioo  15297  uspgrf1oedg  16046  usgr0vb  16103  bj-nnbidc  16404  bj-prexg  16557  strcollnft  16630