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  4349  posng  4847  sosng  4848  optocl  4851  xpexcnvm  5142  relcnvexb  5327  funimass1  5458  dmfex  5582  f1ocnvb  5653  eqfnfv2  5807  elpreima  5828  dff13  5974  f1ocnvfv  5985  f1ocnvfvb  5986  fliftfun  6002  eusvobj2  6071  mpoxopn0yelv  6510  rntpos  6528  erexb  6832  findcard2  7193  findcard2s  7194  xpfi  7239  sbthlemi3  7276  enq0tr  7801  addnqprllem  7894  addnqprulem  7895  distrlem1prl  7949  distrlem1pru  7950  recexprlem1ssl  8000  recexprlem1ssu  8001  elrealeu  8196  addcan  8506  addcan2  8507  neg11  8577  negreb  8591  mulcanapd  8989  receuap  8999  cju  9291  nn1suc  9323  nnaddcl  9324  nndivtr  9346  znegclb  9677  zaddcllempos  9681  zmulcl  9698  zeo  9751  uz11  9945  uzp1  9956  eqreznegel  10014  xneg11  10236  xnegdi  10270  modqadd1  10798  modqmul1  10814  frec2uzltd  10840  bccmpl  11192  bcm1n  11207  fz1eqb  11229  eqwrd  11345  ccatopth  11488  ccatopth2  11489  swrdccatin2  11501  cj11  11671  rennim  11768  resqrexlemgt0  11786  efne0  12445  dvdsabseq  12614  pcfac  13129  divsfval  13649  grpinveu  13843  mulgass  13962  dvreq1  14449  unitrrg  14576  uptx  15375  hmeocnvb  15419  tgioo  15655  uspgrf1oedg  16417  usgr0vb  16474  bj-nnbidc  16785  bj-prexg  16937  strcollnft  17010