Theorem syl5ib 210

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

Syntax hints:   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  syl5ibcom  211  syl5ibr  212  19.23tOLD  1819  nfsb4t  2080  ax11indalem  2197  ax11inda2ALT  2198  gencl  2887  spsbc  3058  eqsbc3r  3103  ssnelpss  3613  adj11  3889  uniintsn  3963  phi011lem1  4598  optocl  4838  xpexr  5109  funimass1  5169  fneu  5187  dmfex  5247  fniniseg  5371  eqfnfv  5392  eqfnfv2  5393  elpreima  5407  fnasrn  5417  dffo4  5423  fconst5  5455  funiunfv  5467  dff13  5471  f1ocnvfv  5478  f1ocnvfvb  5479  ce0ncpw1  6185  cecl  6186  dflec3  6221  lenc  6223