Theorem imbitrid 154

Description: A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.)

Hypotheses

Ref	Expression
imbitrid.1	|- ( ph -> ps )
imbitrid.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
imbitrid	|- ( ch -> ( ph -> th ) )

Proof of Theorem imbitrid

Step	Hyp	Ref	Expression
1		imbitrid.1	. 2 |- ( ph -> ps )
2		imbitrid.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	2	biimpd 144	. 2 |- ( ch -> ( ps -> th ) )
4	1, 3	syl5 32	1 |- ( ch -> ( ph -> th ) )

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl5ibcom  155  imbitrrid  156  sbft  1862  gencl  2795  spsbc  3001  prexg  4245  posng  4736  sosng  4737  optocl  4740  relcnvexb  5210  funimass1  5336  dmfex  5450  f1ocnvb  5521  eqfnfv2  5663  elpreima  5684  dff13  5818  f1ocnvfv  5829  f1ocnvfvb  5830  fliftfun  5846  eusvobj2  5911  mpoxopn0yelv  6306  rntpos  6324  erexb  6626  findcard2  6959  findcard2s  6960  xpfi  7002  sbthlemi3  7034  enq0tr  7518  addnqprllem  7611  addnqprulem  7612  distrlem1prl  7666  distrlem1pru  7667  recexprlem1ssl  7717  recexprlem1ssu  7718  elrealeu  7913  addcan  8223  addcan2  8224  neg11  8294  negreb  8308  mulcanapd  8705  receuap  8713  cju  9005  nn1suc  9026  nnaddcl  9027  nndivtr  9049  znegclb  9376  zaddcllempos  9380  zmulcl  9396  zeo  9448  uz11  9641  uzp1  9652  eqreznegel  9705  xneg11  9926  xnegdi  9960  modqadd1  10470  modqmul1  10486  frec2uzltd  10512  bccmpl  10863  fz1eqb  10899  eqwrd  10992  cj11  11087  rennim  11184  resqrexlemgt0  11202  efne0  11860  dvdsabseq  12029  pcfac  12544  divsfval  13030  grpinveu  13240  mulgass  13365  dvreq1  13774  unitrrg  13899  uptx  14594  hmeocnvb  14638  tgioo  14874  bj-nnbidc  15487  bj-prexg  15641  strcollnft  15714