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  4196  posng  4683  sosng  4684  optocl  4687  relcnvexb  5150  funimass1  5275  dmfex  5387  f1ocnvb  5456  eqfnfv2  5594  elpreima  5615  dff13  5747  f1ocnvfv  5758  f1ocnvfvb  5759  fliftfun  5775  eusvobj2  5839  mpoxopn0yelv  6218  rntpos  6236  erexb  6538  findcard2  6867  findcard2s  6868  xpfi  6907  sbthlemi3  6936  enq0tr  7396  addnqprllem  7489  addnqprulem  7490  distrlem1prl  7544  distrlem1pru  7545  recexprlem1ssl  7595  recexprlem1ssu  7596  elrealeu  7791  addcan  8099  addcan2  8100  neg11  8170  negreb  8184  mulcanapd  8579  receuap  8587  cju  8877  nn1suc  8897  nnaddcl  8898  nndivtr  8920  znegclb  9245  zaddcllempos  9249  zmulcl  9265  zeo  9317  uz11  9509  uzp1  9520  eqreznegel  9573  xneg11  9791  xnegdi  9825  modqadd1  10317  modqmul1  10333  frec2uzltd  10359  bccmpl  10688  fz1eqb  10725  cj11  10869  rennim  10966  resqrexlemgt0  10984  efne0  11641  dvdsabseq  11807  pcfac  12302  grpinveu  12741  uptx  13068  hmeocnvb  13112  tgioo  13340  bj-nnbidc  13792  bj-prexg  13946  strcollnft  14019