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-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl5ibcom  154  syl5ibr  155  sbft  1787  gencl  2673  spsbc  2873  prexg  4071  posng  4549  sosng  4550  optocl  4553  relcnvexb  5014  funimass1  5136  dmfex  5248  f1ocnvb  5315  eqfnfv2  5451  elpreima  5471  dff13  5601  f1ocnvfv  5612  f1ocnvfvb  5613  fliftfun  5629  eusvobj2  5692  mpoxopn0yelv  6066  rntpos  6084  erexb  6384  findcard2  6712  findcard2s  6713  xpfi  6747  sbthlemi3  6775  enq0tr  7143  addnqprllem  7236  addnqprulem  7237  distrlem1prl  7291  distrlem1pru  7292  recexprlem1ssl  7342  recexprlem1ssu  7343  elrealeu  7517  addcan  7813  addcan2  7814  neg11  7884  negreb  7898  mulcanapd  8283  receuap  8291  cju  8577  nn1suc  8597  nnaddcl  8598  nndivtr  8620  znegclb  8939  zaddcllempos  8943  zmulcl  8959  zeo  9008  uz11  9198  uzp1  9209  eqreznegel  9256  xneg11  9458  xnegdi  9492  modqadd1  9975  modqmul1  9991  frec2uzltd  10017  bccmpl  10341  fz1eqb  10378  cj11  10518  rennim  10614  resqrexlemgt0  10632  efne0  11182  dvdsabseq  11340  uptx  12224  tgioo  12465  bj-prexg  12690  strcollnft  12767