Theorem syl5ib 152

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 142	. 2 |- ( ch -> ( ps -> th ) )
4	1, 3	syl5 32	1 |- ( ch -> ( ph -> th ) )

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  syl5ibcom  153  syl5ibr  154  sbft  1769  gencl  2631  spsbc  2826  prexg  3966  posng  4430  sosng  4431  optocl  4434  relcnvexb  4877  funimass1  4996  dmfex  5099  f1ocnvb  5160  eqfnfv2  5287  elpreima  5307  dff13  5428  f1ocnvfv  5439  f1ocnvfvb  5440  fliftfun  5456  eusvobj2  5518  mpt2xopn0yelv  5877  rntpos  5895  erexb  6154  findcard2  6373  findcard2s  6374  enq0tr  6624  addnqprllem  6717  addnqprulem  6718  distrlem1prl  6772  distrlem1pru  6773  recexprlem1ssl  6823  recexprlem1ssu  6824  elrealeu  6998  addcan  7288  addcan2  7289  neg11  7359  negreb  7373  mulcanapd  7751  receuap  7759  cju  8038  nn1suc  8058  nnaddcl  8059  nndivtr  8080  znegclb  8384  zaddcllempos  8388  zmulcl  8404  zeo  8452  uz11  8641  uzp1  8652  eqreznegel  8699  xneg11  8901  modqadd1  9363  modqmul1  9379  frec2uzltd  9405  bccmpl  9681  cj11  9792  rennim  9888  resqrexlemgt0  9906  dvdsabseq  10247  bj-prexg  10702  strcollnft  10779