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 ⊢ (𝜒 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  syl5ibcom  155  imbitrrid  156  sbft  1901  gencl  2854  spsbc  3063  prexg  4349  posng  4847  sosng  4848  optocl  4851  xpexcnvm  5142  relcnvexb  5327  funimass1  5458  dmfex  5582  f1ocnvb  5653  eqfnfv2  5807  elpreima  5828  dff13  5974  f1ocnvfv  5985  f1ocnvfvb  5986  fliftfun  6002  eusvobj2  6071  mpoxopn0yelv  6510  rntpos  6528  erexb  6832  findcard2  7193  findcard2s  7194  xpfi  7239  sbthlemi3  7276  enq0tr  7801  addnqprllem  7894  addnqprulem  7895  distrlem1prl  7949  distrlem1pru  7950  recexprlem1ssl  8000  recexprlem1ssu  8001  elrealeu  8196  addcan  8506  addcan2  8507  neg11  8577  negreb  8591  mulcanapd  8990  receuap  9000  cju  9292  nn1suc  9324  nnaddcl  9325  nndivtr  9347  znegclb  9679  zaddcllempos  9683  zmulcl  9700  zeo  9753  uz11  9947  uzp1  9958  eqreznegel  10016  xneg11  10238  xnegdi  10272  modqadd1  10800  modqmul1  10816  frec2uzltd  10842  bccmpl  11194  bcm1n  11209  fz1eqb  11231  eqwrd  11347  ccatopth  11490  ccatopth2  11491  swrdccatin2  11503  cj11  11673  rennim  11770  resqrexlemgt0  11788  efne0  12447  dvdsabseq  12616  pcfac  13131  divsfval  13651  grpinveu  13845  mulgass  13964  dvreq1  14451  unitrrg  14578  uptx  15377  hmeocnvb  15421  tgioo  15657  uspgrf1oedg  16429  usgr0vb  16486  bj-nnbidc  16797  bj-prexg  16949  strcollnft  17022