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 ) )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl5ibcom  155  imbitrrid  156  sbft  1894  gencl  2832  spsbc  3040  prexg  4294  posng  4790  sosng  4791  optocl  4794  relcnvexb  5267  funimass1  5397  dmfex  5514  f1ocnvb  5585  eqfnfv2  5732  elpreima  5753  dff13  5891  f1ocnvfv  5902  f1ocnvfvb  5903  fliftfun  5919  eusvobj2  5986  mpoxopn0yelv  6383  rntpos  6401  erexb  6703  findcard2  7047  findcard2s  7048  xpfi  7090  sbthlemi3  7122  enq0tr  7617  addnqprllem  7710  addnqprulem  7711  distrlem1prl  7765  distrlem1pru  7766  recexprlem1ssl  7816  recexprlem1ssu  7817  elrealeu  8012  addcan  8322  addcan2  8323  neg11  8393  negreb  8407  mulcanapd  8804  receuap  8812  cju  9104  nn1suc  9125  nnaddcl  9126  nndivtr  9148  znegclb  9475  zaddcllempos  9479  zmulcl  9496  zeo  9548  uz11  9741  uzp1  9752  eqreznegel  9805  xneg11  10026  xnegdi  10060  modqadd1  10578  modqmul1  10594  frec2uzltd  10620  bccmpl  10971  fz1eqb  11007  eqwrd  11107  ccatopth  11243  ccatopth2  11244  swrdccatin2  11256  cj11  11411  rennim  11508  resqrexlemgt0  11526  efne0  12184  dvdsabseq  12353  pcfac  12868  divsfval  13356  grpinveu  13566  mulgass  13691  dvreq1  14100  unitrrg  14225  uptx  14942  hmeocnvb  14986  tgioo  15222  uspgrf1oedg  15968  bj-nnbidc  16079  bj-prexg  16232  strcollnft  16305