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  1870  gencl  2803  spsbc  3009  prexg  4254  posng  4746  sosng  4747  optocl  4750  relcnvexb  5221  funimass1  5350  dmfex  5464  f1ocnvb  5535  eqfnfv2  5677  elpreima  5698  dff13  5836  f1ocnvfv  5847  f1ocnvfvb  5848  fliftfun  5864  eusvobj2  5929  mpoxopn0yelv  6324  rntpos  6342  erexb  6644  findcard2  6985  findcard2s  6986  xpfi  7028  sbthlemi3  7060  enq0tr  7546  addnqprllem  7639  addnqprulem  7640  distrlem1prl  7694  distrlem1pru  7695  recexprlem1ssl  7745  recexprlem1ssu  7746  elrealeu  7941  addcan  8251  addcan2  8252  neg11  8322  negreb  8336  mulcanapd  8733  receuap  8741  cju  9033  nn1suc  9054  nnaddcl  9055  nndivtr  9077  znegclb  9404  zaddcllempos  9408  zmulcl  9425  zeo  9477  uz11  9670  uzp1  9681  eqreznegel  9734  xneg11  9955  xnegdi  9989  modqadd1  10504  modqmul1  10520  frec2uzltd  10546  bccmpl  10897  fz1eqb  10933  eqwrd  11032  cj11  11187  rennim  11284  resqrexlemgt0  11302  efne0  11960  dvdsabseq  12129  pcfac  12644  divsfval  13131  grpinveu  13341  mulgass  13466  dvreq1  13875  unitrrg  14000  uptx  14717  hmeocnvb  14761  tgioo  14997  bj-nnbidc  15655  bj-prexg  15809  strcollnft  15882