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  1820  gencl  2718  spsbc  2920  prexg  4133  posng  4611  sosng  4612  optocl  4615  relcnvexb  5078  funimass1  5200  dmfex  5312  f1ocnvb  5381  eqfnfv2  5519  elpreima  5539  dff13  5669  f1ocnvfv  5680  f1ocnvfvb  5681  fliftfun  5697  eusvobj2  5760  mpoxopn0yelv  6136  rntpos  6154  erexb  6454  findcard2  6783  findcard2s  6784  xpfi  6818  sbthlemi3  6847  enq0tr  7242  addnqprllem  7335  addnqprulem  7336  distrlem1prl  7390  distrlem1pru  7391  recexprlem1ssl  7441  recexprlem1ssu  7442  elrealeu  7637  addcan  7942  addcan2  7943  neg11  8013  negreb  8027  mulcanapd  8422  receuap  8430  cju  8719  nn1suc  8739  nnaddcl  8740  nndivtr  8762  znegclb  9087  zaddcllempos  9091  zmulcl  9107  zeo  9156  uz11  9348  uzp1  9359  eqreznegel  9406  xneg11  9617  xnegdi  9651  modqadd1  10134  modqmul1  10150  frec2uzltd  10176  bccmpl  10500  fz1eqb  10537  cj11  10677  rennim  10774  resqrexlemgt0  10792  efne0  11384  dvdsabseq  11545  uptx  12443  hmeocnvb  12487  tgioo  12715  bj-nnbidc  12962  bj-prexg  13109  strcollnft  13182