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  6515  rntpos  6533  erexb  6837  findcard2  7199  findcard2s  7200  xpfi  7245  sbthlemi3  7283  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  9686  zaddcllempos  9690  zmulcl  9707  zeo  9761  uz11  9960  uzp1  9971  eqreznegel  10029  xneg11  10252  xnegdi  10286  modqadd1  10818  modqmul1  10834  frec2uzltd  10860  bccmpl  11213  bcm1n  11228  fz1eqb  11250  eqwrd  11366  ccatopth  11509  ccatopth2  11510  swrdccatin2  11522  cj11  11692  rennim  11789  resqrexlemgt0  11807  efne0  12469  dvdsabseq  12638  pcfac  13157  divsfval  13707  grpinveu  13901  mulgass  14020  dvreq1  14557  unitrrg  14684  uptx  15517  hmeocnvb  15561  tgioo  15797  uspgrf1oedg  16639  usgr0vb  16696  bj-nnbidc  17007  bj-prexg  17159  strcollnft  17232