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  6416  addnqprllem  6509  addnqprulem  6510  distrlem1prl  6557  distrlem1pru  6558  recexprlem1ssl  6604  recexprlem1ssu  6605  addcan  6968  addcan2  6969  neg11  7038  negreb  7052  mulcanapd  7404  receuap  7412  cju  7674  nn1suc  7694  nnaddcl  7695  nndivtr  7716  znegclb  8034  zaddcllempos  8038  zmulcl  8053  zeo  8099  uz11  8251  uzp1  8262  eqreznegel  8305  xneg11  8497  frec2uzltd  8850  cj11  9113  rennim  9191  bj-prexg  9342  strcollnft  9414