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  1901  gencl  2854  spsbc  3063  prexg  4344  posng  4842  sosng  4843  optocl  4846  xpexcnvm  5137  relcnvexb  5322  funimass1  5453  dmfex  5577  f1ocnvb  5648  eqfnfv2  5798  elpreima  5819  dff13  5964  f1ocnvfv  5975  f1ocnvfvb  5976  fliftfun  5992  eusvobj2  6061  mpoxopn0yelv  6500  rntpos  6518  erexb  6822  findcard2  7183  findcard2s  7184  xpfi  7229  sbthlemi3  7266  enq0tr  7791  addnqprllem  7884  addnqprulem  7885  distrlem1prl  7939  distrlem1pru  7940  recexprlem1ssl  7990  recexprlem1ssu  7991  elrealeu  8186  addcan  8496  addcan2  8497  neg11  8567  negreb  8581  mulcanapd  8979  receuap  8989  cju  9281  nn1suc  9302  nnaddcl  9303  nndivtr  9325  znegclb  9656  zaddcllempos  9660  zmulcl  9677  zeo  9730  uz11  9924  uzp1  9935  eqreznegel  9993  xneg11  10215  xnegdi  10249  modqadd1  10776  modqmul1  10792  frec2uzltd  10818  bccmpl  11170  bcm1n  11185  fz1eqb  11207  eqwrd  11323  ccatopth  11466  ccatopth2  11467  swrdccatin2  11479  cj11  11649  rennim  11746  resqrexlemgt0  11764  efne0  12423  dvdsabseq  12592  pcfac  13107  divsfval  13626  grpinveu  13820  mulgass  13939  dvreq1  14422  unitrrg  14549  uptx  15298  hmeocnvb  15342  tgioo  15578  uspgrf1oedg  16331  usgr0vb  16388  bj-nnbidc  16699  bj-prexg  16851  strcollnft  16924