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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  syl5ibcom  155  imbitrrid  156  sbft  1901  gencl  2854  spsbc  3063  prexg  4351  posng  4849  sosng  4850  optocl  4853  xpexcnvm  5145  relcnvexb  5330  funimass1  5461  dmfex  5585  f1ocnvb  5656  eqfnfv2  5810  elpreima  5831  dff13  5977  f1ocnvfv  5988  f1ocnvfvb  5989  fliftfun  6005  eusvobj2  6074  mpoxopn0yelv  6514  rntpos  6532  erexb  6836  findcard2  7197  findcard2s  7198  xpfi  7243  sbthlemi3  7281  enq0tr  7807  addnqprllem  7900  addnqprulem  7901  distrlem1prl  7955  distrlem1pru  7956  recexprlem1ssl  8006  recexprlem1ssu  8007  elrealeu  8202  addcan  8513  addcan2  8514  neg11  8584  negreb  8598  mulcanapd  8997  receuap  9007  cju  9299  nn1suc  9332  nnaddcl  9333  nndivtr  9355  znegclb  9688  zaddcllempos  9692  zmulcl  9709  zeo  9762  uz11  9961  uzp1  9972  eqreznegel  10030  xneg11  10253  xnegdi  10287  modqadd1  10819  modqmul1  10835  frec2uzltd  10861  bccmpl  11214  bcm1n  11229  fz1eqb  11251  eqwrd  11367  ccatopth  11510  ccatopth2  11511  swrdccatin2  11523  cj11  11693  rennim  11790  resqrexlemgt0  11808  efne0  12470  dvdsabseq  12639  pcfac  13158  divsfval  13708  grpinveu  13902  mulgass  14021  dvreq1  14558  unitrrg  14685  uptx  15500  hmeocnvb  15544  tgioo  15780  uspgrf1oedg  16622  usgr0vb  16679  bj-nnbidc  16990  bj-prexg  17142  strcollnft  17215