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  10813  modqmul1  10829  frec2uzltd  10855  bccmpl  11208  bcm1n  11223  fz1eqb  11245  eqwrd  11361  ccatopth  11504  ccatopth2  11505  swrdccatin2  11517  cj11  11687  rennim  11784  resqrexlemgt0  11802  efne0  12464  dvdsabseq  12633  pcfac  13152  divsfval  13702  grpinveu  13896  mulgass  14015  dvreq1  14533  unitrrg  14660  uptx  15466  hmeocnvb  15510  tgioo  15746  uspgrf1oedg  16583  usgr0vb  16640  bj-nnbidc  16951  bj-prexg  17103  strcollnft  17176