Theorem syl5ib 153

Description: A mixed syllogism inference. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl5ib.1	|- ( ph -> ps )
syl5ib.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
syl5ib	|- ( ch -> ( ph -> th ) )

Proof of Theorem syl5ib

Step	Hyp	Ref	Expression
1		syl5ib.1	. 2 |- ( ph -> ps )
2		syl5ib.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	2	biimpd 143	. 2 |- ( ch -> ( ps -> th ) )
4	1, 3	syl5 32	1 |- ( ch -> ( ph -> th ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl5ibcom  154  syl5ibr  155  sbft  1820  gencl  2713  spsbc  2915  prexg  4128  posng  4606  sosng  4607  optocl  4610  relcnvexb  5073  funimass1  5195  dmfex  5307  f1ocnvb  5374  eqfnfv2  5512  elpreima  5532  dff13  5662  f1ocnvfv  5673  f1ocnvfvb  5674  fliftfun  5690  eusvobj2  5753  mpoxopn0yelv  6129  rntpos  6147  erexb  6447  findcard2  6776  findcard2s  6777  xpfi  6811  sbthlemi3  6840  enq0tr  7235  addnqprllem  7328  addnqprulem  7329  distrlem1prl  7383  distrlem1pru  7384  recexprlem1ssl  7434  recexprlem1ssu  7435  elrealeu  7630  addcan  7935  addcan2  7936  neg11  8006  negreb  8020  mulcanapd  8415  receuap  8423  cju  8712  nn1suc  8732  nnaddcl  8733  nndivtr  8755  znegclb  9080  zaddcllempos  9084  zmulcl  9100  zeo  9149  uz11  9341  uzp1  9352  eqreznegel  9399  xneg11  9610  xnegdi  9644  modqadd1  10127  modqmul1  10143  frec2uzltd  10169  bccmpl  10493  fz1eqb  10530  cj11  10670  rennim  10767  resqrexlemgt0  10785  efne0  11373  dvdsabseq  11534  uptx  12432  hmeocnvb  12476  tgioo  12704  bj-nnbidc  12951  bj-prexg  13098  strcollnft  13171