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  2848  spsbc  3057  prexg  4330  posng  4827  sosng  4828  optocl  4831  xpexcnvm  5122  relcnvexb  5307  funimass1  5438  dmfex  5562  f1ocnvb  5633  eqfnfv2  5781  elpreima  5802  dff13  5947  f1ocnvfv  5958  f1ocnvfvb  5959  fliftfun  5975  eusvobj2  6044  mpoxopn0yelv  6483  rntpos  6501  erexb  6805  findcard2  7159  findcard2s  7160  xpfi  7205  sbthlemi3  7242  enq0tr  7765  addnqprllem  7858  addnqprulem  7859  distrlem1prl  7913  distrlem1pru  7914  recexprlem1ssl  7964  recexprlem1ssu  7965  elrealeu  8160  addcan  8469  addcan2  8470  neg11  8540  negreb  8554  mulcanapd  8952  receuap  8960  cju  9252  nn1suc  9273  nnaddcl  9274  nndivtr  9296  znegclb  9627  zaddcllempos  9631  zmulcl  9648  zeo  9701  uz11  9895  uzp1  9906  eqreznegel  9964  xneg11  10186  xnegdi  10220  modqadd1  10747  modqmul1  10763  frec2uzltd  10789  bccmpl  11141  bcm1n  11156  fz1eqb  11178  eqwrd  11290  ccatopth  11433  ccatopth2  11434  swrdccatin2  11446  cj11  11615  rennim  11712  resqrexlemgt0  11730  efne0  12389  dvdsabseq  12558  pcfac  13073  divsfval  13592  grpinveu  13793  mulgass  13912  dvreq1  14387  unitrrg  14514  uptx  15265  hmeocnvb  15309  tgioo  15545  uspgrf1oedg  16297  usgr0vb  16354  bj-nnbidc  16655  bj-prexg  16807  strcollnft  16880