Theorem syl5ib 153

Description: A mixed syllogism inference. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl5ib.1	⊢ (𝜑 → 𝜓)
syl5ib.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5ib	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem syl5ib

Step	Hyp	Ref	Expression
1		syl5ib.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl5ib.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	2	biimpd 143	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	1, 3	syl5 32	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl5ibcom  154  syl5ibr  155  sbft  1821  gencl  2721  spsbc  2924  prexg  4141  posng  4619  sosng  4620  optocl  4623  relcnvexb  5086  funimass1  5208  dmfex  5320  f1ocnvb  5389  eqfnfv2  5527  elpreima  5547  dff13  5677  f1ocnvfv  5688  f1ocnvfvb  5689  fliftfun  5705  eusvobj2  5768  mpoxopn0yelv  6144  rntpos  6162  erexb  6462  findcard2  6791  findcard2s  6792  xpfi  6826  sbthlemi3  6855  enq0tr  7266  addnqprllem  7359  addnqprulem  7360  distrlem1prl  7414  distrlem1pru  7415  recexprlem1ssl  7465  recexprlem1ssu  7466  elrealeu  7661  addcan  7966  addcan2  7967  neg11  8037  negreb  8051  mulcanapd  8446  receuap  8454  cju  8743  nn1suc  8763  nnaddcl  8764  nndivtr  8786  znegclb  9111  zaddcllempos  9115  zmulcl  9131  zeo  9180  uz11  9372  uzp1  9383  eqreznegel  9433  xneg11  9647  xnegdi  9681  modqadd1  10165  modqmul1  10181  frec2uzltd  10207  bccmpl  10532  fz1eqb  10569  cj11  10709  rennim  10806  resqrexlemgt0  10824  efne0  11421  dvdsabseq  11581  uptx  12482  hmeocnvb  12526  tgioo  12754  bj-nnbidc  13133  bj-prexg  13280  strcollnft  13353