Theorem imbitrid 154

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

Hypotheses

Ref	Expression
imbitrid.1	⊢ (𝜑 → 𝜓)
imbitrid.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
imbitrid	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem imbitrid

Step	Hyp	Ref	Expression
1		imbitrid.1	. 2 ⊢ (𝜑 → 𝜓)
2		imbitrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	2	biimpd 144	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	1, 3	syl5 32	1 ⊢ (𝜒 → (𝜑 → 𝜃))

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  1874  gencl  2812  spsbc  3020  prexg  4274  posng  4768  sosng  4769  optocl  4772  relcnvexb  5244  funimass1  5374  dmfex  5491  f1ocnvb  5562  eqfnfv2  5706  elpreima  5727  dff13  5865  f1ocnvfv  5876  f1ocnvfvb  5877  fliftfun  5893  eusvobj2  5960  mpoxopn0yelv  6355  rntpos  6373  erexb  6675  findcard2  7019  findcard2s  7020  xpfi  7062  sbthlemi3  7094  enq0tr  7589  addnqprllem  7682  addnqprulem  7683  distrlem1prl  7737  distrlem1pru  7738  recexprlem1ssl  7788  recexprlem1ssu  7789  elrealeu  7984  addcan  8294  addcan2  8295  neg11  8365  negreb  8379  mulcanapd  8776  receuap  8784  cju  9076  nn1suc  9097  nnaddcl  9098  nndivtr  9120  znegclb  9447  zaddcllempos  9451  zmulcl  9468  zeo  9520  uz11  9713  uzp1  9724  eqreznegel  9777  xneg11  9998  xnegdi  10032  modqadd1  10550  modqmul1  10566  frec2uzltd  10592  bccmpl  10943  fz1eqb  10979  eqwrd  11078  ccatopth  11214  ccatopth2  11215  swrdccatin2  11227  cj11  11382  rennim  11479  resqrexlemgt0  11497  efne0  12155  dvdsabseq  12324  pcfac  12839  divsfval  13327  grpinveu  13537  mulgass  13662  dvreq1  14071  unitrrg  14196  uptx  14913  hmeocnvb  14957  tgioo  15193  uspgrf1oedg  15939  bj-nnbidc  16031  bj-prexg  16184  strcollnft  16257