Theorem syl5ib 143

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 132	. 2 ⊢ (χ → (ψ → θ))
4	1, 3	syl5 28	1 ⊢ (χ → (φ → θ))

Syntax hints:   → wi 4   ↔ wb 98

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  syl5ibcom  144  syl5ibr  145  sbft  1725  gencl  2580  spsbc  2769  eqsbc3r  2813  ssnelpss  3283  prexgOLD  3937  prexg  3938  posng  4355  sosng  4356  optocl  4359  relcnvexb  4800  funimass1  4919  dmfex  5022  f1ocnvb  5083  eqfnfv2  5209  elpreima  5229  dff13  5350  f1ocnvfv  5362  f1ocnvfvb  5363  fliftfun  5379  eusvobj2  5441  mpt2xopn0yelv  5795  rntpos  5813  erexb  6067  enq0tr  6417  addnqprllem  6510  addnqprulem  6511  distrlem1prl  6558  distrlem1pru  6559  recexprlem1ssl  6605  recexprlem1ssu  6606  addcan  6988  addcan2  6989  neg11  7058  negreb  7072  mulcanapd  7424  receuap  7432  cju  7694  nn1suc  7714  nnaddcl  7715  nndivtr  7736  znegclb  8054  zaddcllempos  8058  zmulcl  8073  zeo  8119  uz11  8271  uzp1  8282  eqreznegel  8325  xneg11  8517  frec2uzltd  8870  cj11  9133  rennim  9211  bj-prexg  9366  strcollnft  9444