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  2832  spsbc  3040  prexg  4295  posng  4791  sosng  4792  optocl  4795  relcnvexb  5268  funimass1  5398  dmfex  5517  f1ocnvb  5588  eqfnfv2  5735  elpreima  5756  dff13  5898  f1ocnvfv  5909  f1ocnvfvb  5910  fliftfun  5926  eusvobj2  5993  mpoxopn0yelv  6391  rntpos  6409  erexb  6713  findcard2  7059  findcard2s  7060  xpfi  7105  sbthlemi3  7137  enq0tr  7632  addnqprllem  7725  addnqprulem  7726  distrlem1prl  7780  distrlem1pru  7781  recexprlem1ssl  7831  recexprlem1ssu  7832  elrealeu  8027  addcan  8337  addcan2  8338  neg11  8408  negreb  8422  mulcanapd  8819  receuap  8827  cju  9119  nn1suc  9140  nnaddcl  9141  nndivtr  9163  znegclb  9490  zaddcllempos  9494  zmulcl  9511  zeo  9563  uz11  9757  uzp1  9768  eqreznegel  9821  xneg11  10042  xnegdi  10076  modqadd1  10595  modqmul1  10611  frec2uzltd  10637  bccmpl  10988  fz1eqb  11024  eqwrd  11125  ccatopth  11263  ccatopth2  11264  swrdccatin2  11276  cj11  11431  rennim  11528  resqrexlemgt0  11546  efne0  12204  dvdsabseq  12373  pcfac  12888  divsfval  13376  grpinveu  13586  mulgass  13711  dvreq1  14121  unitrrg  14246  uptx  14963  hmeocnvb  15007  tgioo  15243  uspgrf1oedg  15989  bj-nnbidc  16176  bj-prexg  16329  strcollnft  16402