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  3056  prexg  4327  posng  4824  sosng  4825  optocl  4828  xpexcnvm  5119  relcnvexb  5304  funimass1  5435  dmfex  5559  f1ocnvb  5630  eqfnfv2  5778  elpreima  5799  dff13  5943  f1ocnvfv  5954  f1ocnvfvb  5955  fliftfun  5971  eusvobj2  6038  mpoxopn0yelv  6472  rntpos  6490  erexb  6794  findcard2  7148  findcard2s  7149  xpfi  7194  sbthlemi3  7231  enq0tr  7754  addnqprllem  7847  addnqprulem  7848  distrlem1prl  7902  distrlem1pru  7903  recexprlem1ssl  7953  recexprlem1ssu  7954  elrealeu  8149  addcan  8458  addcan2  8459  neg11  8529  negreb  8543  mulcanapd  8940  receuap  8948  cju  9240  nn1suc  9261  nnaddcl  9262  nndivtr  9284  znegclb  9615  zaddcllempos  9619  zmulcl  9636  zeo  9689  uz11  9883  uzp1  9894  eqreznegel  9952  xneg11  10173  xnegdi  10207  modqadd1  10730  modqmul1  10746  frec2uzltd  10772  bccmpl  11124  bcm1n  11139  fz1eqb  11161  eqwrd  11273  ccatopth  11416  ccatopth2  11417  swrdccatin2  11429  cj11  11598  rennim  11695  resqrexlemgt0  11713  efne0  12372  dvdsabseq  12541  pcfac  13056  divsfval  13562  grpinveu  13772  mulgass  13897  dvreq1  14309  unitrrg  14436  uptx  15188  hmeocnvb  15232  tgioo  15468  uspgrf1oedg  16220  usgr0vb  16277  bj-nnbidc  16578  bj-prexg  16730  strcollnft  16803