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-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl5ibcom  154  syl5ibr  155  sbft  1777  gencl  2652  spsbc  2852  prexg  4047  posng  4523  sosng  4524  optocl  4527  relcnvexb  4983  funimass1  5104  dmfex  5213  f1ocnvb  5280  eqfnfv2  5412  elpreima  5432  dff13  5561  f1ocnvfv  5572  f1ocnvfvb  5573  fliftfun  5589  eusvobj2  5652  mpt2xopn0yelv  6018  rntpos  6036  erexb  6331  findcard2  6659  findcard2s  6660  xpfi  6694  sbthlemi3  6722  enq0tr  7047  addnqprllem  7140  addnqprulem  7141  distrlem1prl  7195  distrlem1pru  7196  recexprlem1ssl  7246  recexprlem1ssu  7247  elrealeu  7421  addcan  7716  addcan2  7717  neg11  7787  negreb  7801  mulcanapd  8184  receuap  8192  cju  8475  nn1suc  8495  nnaddcl  8496  nndivtr  8518  znegclb  8837  zaddcllempos  8841  zmulcl  8857  zeo  8905  uz11  9095  uzp1  9106  eqreznegel  9153  xneg11  9350  modqadd1  9822  modqmul1  9838  frec2uzltd  9864  bccmpl  10216  fz1eqb  10253  cj11  10393  rennim  10489  resqrexlemgt0  10507  efne0  11022  dvdsabseq  11180  bj-prexg  12068  strcollnft  12145