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  1848  gencl  2770  spsbc  2975  prexg  4212  posng  4699  sosng  4700  optocl  4703  relcnvexb  5169  funimass1  5294  dmfex  5406  f1ocnvb  5476  eqfnfv2  5615  elpreima  5636  dff13  5769  f1ocnvfv  5780  f1ocnvfvb  5781  fliftfun  5797  eusvobj2  5861  mpoxopn0yelv  6240  rntpos  6258  erexb  6560  findcard2  6889  findcard2s  6890  xpfi  6929  sbthlemi3  6958  enq0tr  7433  addnqprllem  7526  addnqprulem  7527  distrlem1prl  7581  distrlem1pru  7582  recexprlem1ssl  7632  recexprlem1ssu  7633  elrealeu  7828  addcan  8137  addcan2  8138  neg11  8208  negreb  8222  mulcanapd  8618  receuap  8626  cju  8918  nn1suc  8938  nnaddcl  8939  nndivtr  8961  znegclb  9286  zaddcllempos  9290  zmulcl  9306  zeo  9358  uz11  9550  uzp1  9561  eqreznegel  9614  xneg11  9834  xnegdi  9868  modqadd1  10361  modqmul1  10377  frec2uzltd  10403  bccmpl  10734  fz1eqb  10770  cj11  10914  rennim  11011  resqrexlemgt0  11029  efne0  11686  dvdsabseq  11853  pcfac  12348  grpinveu  12911  mulgass  13020  dvreq1  13311  uptx  13777  hmeocnvb  13821  tgioo  14049  bj-nnbidc  14512  bj-prexg  14666  strcollnft  14739