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  1894  gencl  2833  spsbc  3041  prexg  4299  posng  4796  sosng  4797  optocl  4800  relcnvexb  5274  funimass1  5404  dmfex  5523  f1ocnvb  5594  eqfnfv2  5741  elpreima  5762  dff13  5904  f1ocnvfv  5915  f1ocnvfvb  5916  fliftfun  5932  eusvobj2  5999  mpoxopn0yelv  6400  rntpos  6418  erexb  6722  findcard2  7071  findcard2s  7072  xpfi  7117  sbthlemi3  7149  enq0tr  7644  addnqprllem  7737  addnqprulem  7738  distrlem1prl  7792  distrlem1pru  7793  recexprlem1ssl  7843  recexprlem1ssu  7844  elrealeu  8039  addcan  8349  addcan2  8350  neg11  8420  negreb  8434  mulcanapd  8831  receuap  8839  cju  9131  nn1suc  9152  nnaddcl  9153  nndivtr  9175  znegclb  9502  zaddcllempos  9506  zmulcl  9523  zeo  9575  uz11  9769  uzp1  9780  eqreznegel  9838  xneg11  10059  xnegdi  10093  modqadd1  10613  modqmul1  10629  frec2uzltd  10655  bccmpl  11006  fz1eqb  11042  eqwrd  11144  ccatopth  11287  ccatopth2  11288  swrdccatin2  11300  cj11  11456  rennim  11553  resqrexlemgt0  11571  efne0  12229  dvdsabseq  12398  pcfac  12913  divsfval  13401  grpinveu  13611  mulgass  13736  dvreq1  14146  unitrrg  14271  uptx  14988  hmeocnvb  15032  tgioo  15268  uspgrf1oedg  16015  usgr0vb  16072  bj-nnbidc  16289  bj-prexg  16442  strcollnft  16515