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  2998  prexg  4241  posng  4732  sosng  4733  optocl  4736  relcnvexb  5206  funimass1  5332  dmfex  5444  f1ocnvb  5515  eqfnfv2  5657  elpreima  5678  dff13  5812  f1ocnvfv  5823  f1ocnvfvb  5824  fliftfun  5840  eusvobj2  5905  mpoxopn0yelv  6294  rntpos  6312  erexb  6614  findcard2  6947  findcard2s  6948  xpfi  6988  sbthlemi3  7020  enq0tr  7496  addnqprllem  7589  addnqprulem  7590  distrlem1prl  7644  distrlem1pru  7645  recexprlem1ssl  7695  recexprlem1ssu  7696  elrealeu  7891  addcan  8201  addcan2  8202  neg11  8272  negreb  8286  mulcanapd  8682  receuap  8690  cju  8982  nn1suc  9003  nnaddcl  9004  nndivtr  9026  znegclb  9353  zaddcllempos  9357  zmulcl  9373  zeo  9425  uz11  9618  uzp1  9629  eqreznegel  9682  xneg11  9903  xnegdi  9937  modqadd1  10435  modqmul1  10451  frec2uzltd  10477  bccmpl  10828  fz1eqb  10864  eqwrd  10957  cj11  11052  rennim  11149  resqrexlemgt0  11167  efne0  11824  dvdsabseq  11992  pcfac  12491  divsfval  12914  grpinveu  13113  mulgass  13232  dvreq1  13641  unitrrg  13766  uptx  14453  hmeocnvb  14497  tgioo  14733  bj-nnbidc  15319  bj-prexg  15473  strcollnft  15546