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  1895  gencl  2834  spsbc  3042  prexg  4303  posng  4800  sosng  4801  optocl  4804  relcnvexb  5278  funimass1  5409  dmfex  5529  f1ocnvb  5600  eqfnfv2  5748  elpreima  5769  dff13  5914  f1ocnvfv  5925  f1ocnvfvb  5926  fliftfun  5942  eusvobj2  6009  mpoxopn0yelv  6410  rntpos  6428  erexb  6732  findcard2  7083  findcard2s  7084  xpfi  7129  sbthlemi3  7163  enq0tr  7659  addnqprllem  7752  addnqprulem  7753  distrlem1prl  7807  distrlem1pru  7808  recexprlem1ssl  7858  recexprlem1ssu  7859  elrealeu  8054  addcan  8364  addcan2  8365  neg11  8435  negreb  8449  mulcanapd  8846  receuap  8854  cju  9146  nn1suc  9167  nnaddcl  9168  nndivtr  9190  znegclb  9517  zaddcllempos  9521  zmulcl  9538  zeo  9590  uz11  9784  uzp1  9795  eqreznegel  9853  xneg11  10074  xnegdi  10108  modqadd1  10629  modqmul1  10645  frec2uzltd  10671  bccmpl  11022  fz1eqb  11058  eqwrd  11163  ccatopth  11306  ccatopth2  11307  swrdccatin2  11319  cj11  11488  rennim  11585  resqrexlemgt0  11603  efne0  12262  dvdsabseq  12431  pcfac  12946  divsfval  13434  grpinveu  13644  mulgass  13769  dvreq1  14180  unitrrg  14305  uptx  15027  hmeocnvb  15071  tgioo  15307  uspgrf1oedg  16056  usgr0vb  16113  bj-nnbidc  16414  bj-prexg  16566  strcollnft  16639