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  1841  gencl  2762  spsbc  2966  prexg  4194  posng  4681  sosng  4682  optocl  4685  relcnvexb  5148  funimass1  5273  dmfex  5385  f1ocnvb  5454  eqfnfv2  5592  elpreima  5612  dff13  5744  f1ocnvfv  5755  f1ocnvfvb  5756  fliftfun  5772  eusvobj2  5836  mpoxopn0yelv  6215  rntpos  6233  erexb  6534  findcard2  6863  findcard2s  6864  xpfi  6903  sbthlemi3  6932  enq0tr  7383  addnqprllem  7476  addnqprulem  7477  distrlem1prl  7531  distrlem1pru  7532  recexprlem1ssl  7582  recexprlem1ssu  7583  elrealeu  7778  addcan  8086  addcan2  8087  neg11  8157  negreb  8171  mulcanapd  8566  receuap  8574  cju  8864  nn1suc  8884  nnaddcl  8885  nndivtr  8907  znegclb  9232  zaddcllempos  9236  zmulcl  9252  zeo  9304  uz11  9496  uzp1  9507  eqreznegel  9560  xneg11  9778  xnegdi  9812  modqadd1  10304  modqmul1  10320  frec2uzltd  10346  bccmpl  10675  fz1eqb  10712  cj11  10856  rennim  10953  resqrexlemgt0  10971  efne0  11628  dvdsabseq  11794  pcfac  12289  grpinveu  12728  uptx  13027  hmeocnvb  13071  tgioo  13299  bj-nnbidc  13751  bj-prexg  13906  strcollnft  13979