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  1836  gencl  2758  spsbc  2962  prexg  4189  posng  4676  sosng  4677  optocl  4680  relcnvexb  5143  funimass1  5265  dmfex  5377  f1ocnvb  5446  eqfnfv2  5584  elpreima  5604  dff13  5736  f1ocnvfv  5747  f1ocnvfvb  5748  fliftfun  5764  eusvobj2  5828  mpoxopn0yelv  6207  rntpos  6225  erexb  6526  findcard2  6855  findcard2s  6856  xpfi  6895  sbthlemi3  6924  enq0tr  7375  addnqprllem  7468  addnqprulem  7469  distrlem1prl  7523  distrlem1pru  7524  recexprlem1ssl  7574  recexprlem1ssu  7575  elrealeu  7770  addcan  8078  addcan2  8079  neg11  8149  negreb  8163  mulcanapd  8558  receuap  8566  cju  8856  nn1suc  8876  nnaddcl  8877  nndivtr  8899  znegclb  9224  zaddcllempos  9228  zmulcl  9244  zeo  9296  uz11  9488  uzp1  9499  eqreznegel  9552  xneg11  9770  xnegdi  9804  modqadd1  10296  modqmul1  10312  frec2uzltd  10338  bccmpl  10667  fz1eqb  10704  cj11  10847  rennim  10944  resqrexlemgt0  10962  efne0  11619  dvdsabseq  11785  pcfac  12280  uptx  12924  hmeocnvb  12968  tgioo  13196  bj-nnbidc  13648  bj-prexg  13803  strcollnft  13876