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  8507  addcan2  8508  neg11  8578  negreb  8592  mulcanapd  8991  receuap  9001  cju  9293  nn1suc  9325  nnaddcl  9326  nndivtr  9348  znegclb  9681  zaddcllempos  9685  zmulcl  9702  zeo  9755  uz11  9954  uzp1  9965  eqreznegel  10023  xneg11  10246  xnegdi  10280  modqadd1  10811  modqmul1  10827  frec2uzltd  10853  bccmpl  11206  bcm1n  11221  fz1eqb  11243  eqwrd  11359  ccatopth  11502  ccatopth2  11503  swrdccatin2  11515  cj11  11685  rennim  11782  resqrexlemgt0  11800  efne0  12461  dvdsabseq  12630  pcfac  13149  divsfval  13698  grpinveu  13892  mulgass  14011  dvreq1  14498  unitrrg  14625  uptx  15424  hmeocnvb  15468  tgioo  15704  uspgrf1oedg  16515  usgr0vb  16572  bj-nnbidc  16883  bj-prexg  17035  strcollnft  17108