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  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  8470  addcan2  8471  neg11  8541  negreb  8555  mulcanapd  8953  receuap  8963  cju  9255  nn1suc  9276  nnaddcl  9277  nndivtr  9299  znegclb  9630  zaddcllempos  9634  zmulcl  9651  zeo  9704  uz11  9898  uzp1  9909  eqreznegel  9967  xneg11  10189  xnegdi  10223  modqadd1  10750  modqmul1  10766  frec2uzltd  10792  bccmpl  11144  bcm1n  11159  fz1eqb  11181  eqwrd  11293  ccatopth  11436  ccatopth2  11437  swrdccatin2  11449  cj11  11618  rennim  11715  resqrexlemgt0  11733  efne0  12392  dvdsabseq  12561  pcfac  13076  divsfval  13595  grpinveu  13796  mulgass  13915  dvreq1  14390  unitrrg  14517  uptx  15268  hmeocnvb  15312  tgioo  15548  uspgrf1oedg  16300  usgr0vb  16357  bj-nnbidc  16668  bj-prexg  16820  strcollnft  16893