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  1897  gencl  2846  spsbc  3054  prexg  4325  posng  4822  sosng  4823  optocl  4826  xpexcnvm  5117  relcnvexb  5302  funimass1  5433  dmfex  5557  f1ocnvb  5628  eqfnfv2  5776  elpreima  5797  dff13  5941  f1ocnvfv  5952  f1ocnvfvb  5953  fliftfun  5969  eusvobj2  6036  mpoxopn0yelv  6470  rntpos  6488  erexb  6792  findcard2  7146  findcard2s  7147  xpfi  7192  sbthlemi3  7229  enq0tr  7749  addnqprllem  7842  addnqprulem  7843  distrlem1prl  7897  distrlem1pru  7898  recexprlem1ssl  7948  recexprlem1ssu  7949  elrealeu  8144  addcan  8453  addcan2  8454  neg11  8524  negreb  8538  mulcanapd  8935  receuap  8943  cju  9235  nn1suc  9256  nnaddcl  9257  nndivtr  9279  znegclb  9610  zaddcllempos  9614  zmulcl  9631  zeo  9683  uz11  9877  uzp1  9888  eqreznegel  9946  xneg11  10167  xnegdi  10201  modqadd1  10723  modqmul1  10739  frec2uzltd  10765  bccmpl  11116  bcm1n  11131  fz1eqb  11153  eqwrd  11265  ccatopth  11408  ccatopth2  11409  swrdccatin2  11421  cj11  11590  rennim  11687  resqrexlemgt0  11705  efne0  12364  dvdsabseq  12533  pcfac  13048  divsfval  13541  grpinveu  13751  mulgass  13876  dvreq1  14287  unitrrg  14413  uptx  15139  hmeocnvb  15183  tgioo  15419  uspgrf1oedg  16171  usgr0vb  16228  bj-nnbidc  16529  bj-prexg  16681  strcollnft  16754