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  7802  addnqprllem  7895  addnqprulem  7896  distrlem1prl  7950  distrlem1pru  7951  recexprlem1ssl  8001  recexprlem1ssu  8002  elrealeu  8197  addcan  8508  addcan2  8509  neg11  8579  negreb  8593  mulcanapd  8992  receuap  9002  cju  9294  nn1suc  9326  nnaddcl  9327  nndivtr  9349  znegclb  9682  zaddcllempos  9686  zmulcl  9703  zeo  9756  uz11  9955  uzp1  9966  eqreznegel  10024  xneg11  10247  xnegdi  10281  modqadd1  10812  modqmul1  10828  frec2uzltd  10854  bccmpl  11207  bcm1n  11222  fz1eqb  11244  eqwrd  11360  ccatopth  11503  ccatopth2  11504  swrdccatin2  11516  cj11  11686  rennim  11783  resqrexlemgt0  11801  efne0  12463  dvdsabseq  12632  pcfac  13151  divsfval  13700  grpinveu  13894  mulgass  14013  dvreq1  14500  unitrrg  14627  uptx  15427  hmeocnvb  15471  tgioo  15707  uspgrf1oedg  16539  usgr0vb  16596  bj-nnbidc  16907  bj-prexg  17059  strcollnft  17132