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  1848  gencl  2771  spsbc  2976  prexg  4213  posng  4700  sosng  4701  optocl  4704  relcnvexb  5170  funimass1  5295  dmfex  5407  f1ocnvb  5477  eqfnfv2  5616  elpreima  5637  dff13  5771  f1ocnvfv  5782  f1ocnvfvb  5783  fliftfun  5799  eusvobj2  5863  mpoxopn0yelv  6242  rntpos  6260  erexb  6562  findcard2  6891  findcard2s  6892  xpfi  6931  sbthlemi3  6960  enq0tr  7435  addnqprllem  7528  addnqprulem  7529  distrlem1prl  7583  distrlem1pru  7584  recexprlem1ssl  7634  recexprlem1ssu  7635  elrealeu  7830  addcan  8139  addcan2  8140  neg11  8210  negreb  8224  mulcanapd  8620  receuap  8628  cju  8920  nn1suc  8940  nnaddcl  8941  nndivtr  8963  znegclb  9288  zaddcllempos  9292  zmulcl  9308  zeo  9360  uz11  9552  uzp1  9563  eqreznegel  9616  xneg11  9836  xnegdi  9870  modqadd1  10363  modqmul1  10379  frec2uzltd  10405  bccmpl  10736  fz1eqb  10772  cj11  10916  rennim  11013  resqrexlemgt0  11031  efne0  11688  dvdsabseq  11855  pcfac  12350  grpinveu  12916  mulgass  13025  dvreq1  13316  uptx  13813  hmeocnvb  13857  tgioo  14085  bj-nnbidc  14548  bj-prexg  14702  strcollnft  14775