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  2836  spsbc  3044  prexg  4307  posng  4804  sosng  4805  optocl  4808  xpexcnvm  5098  relcnvexb  5283  funimass1  5414  dmfex  5535  f1ocnvb  5606  eqfnfv2  5754  elpreima  5775  dff13  5919  f1ocnvfv  5930  f1ocnvfvb  5931  fliftfun  5947  eusvobj2  6014  mpoxopn0yelv  6448  rntpos  6466  erexb  6770  findcard2  7121  findcard2s  7122  xpfi  7167  sbthlemi3  7201  enq0tr  7697  addnqprllem  7790  addnqprulem  7791  distrlem1prl  7845  distrlem1pru  7846  recexprlem1ssl  7896  recexprlem1ssu  7897  elrealeu  8092  addcan  8401  addcan2  8402  neg11  8472  negreb  8486  mulcanapd  8883  receuap  8891  cju  9183  nn1suc  9204  nnaddcl  9205  nndivtr  9227  znegclb  9556  zaddcllempos  9560  zmulcl  9577  zeo  9629  uz11  9823  uzp1  9834  eqreznegel  9892  xneg11  10113  xnegdi  10147  modqadd1  10669  modqmul1  10685  frec2uzltd  10711  bccmpl  11062  fz1eqb  11098  eqwrd  11203  ccatopth  11346  ccatopth2  11347  swrdccatin2  11359  cj11  11528  rennim  11625  resqrexlemgt0  11643  efne0  12302  dvdsabseq  12471  pcfac  12986  divsfval  13474  grpinveu  13684  mulgass  13809  dvreq1  14220  unitrrg  14346  uptx  15068  hmeocnvb  15112  tgioo  15348  uspgrf1oedg  16100  usgr0vb  16157  bj-nnbidc  16458  bj-prexg  16610  strcollnft  16683