Theorem sylbid 206

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylbid.1	⊢ (φ → (ψ ↔ χ))
sylbid.2	⊢ (φ → (χ → θ))

Assertion

Ref	Expression
sylbid	⊢ (φ → (ψ → θ))

Proof of Theorem sylbid

Step	Hyp	Ref	Expression
1		sylbid.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	biimpd 198	. 2 ⊢ (φ → (ψ → χ))
3		sylbid.2	. 2 ⊢ (φ → (χ → θ))
4	2, 3	syld 40	1 ⊢ (φ → (ψ → θ))

Syntax hints:   → wi 4   ↔ wb 176

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  3imtr4d  259  ax11eq  2193  ax11el  2194  leltfintr  4458  tfin11  4493  sfinltfin  4535  phi11lem1  4595  xp11  5056  xpcan  5057  xpcan2  5058  enprmaplem3  6078  enprmaplem6  6081  ce0addcnnul  6179  ceclb  6183  fce  6188  sbth  6206  dflec2  6210  lectr  6211  leaddc1  6214  leconnnc  6218  tlecg  6230  letc  6231  ce0lenc1  6239  nclenn  6249  lemuc1  6253  lecadd2  6266  ncslesuc  6267  nchoicelem9  6297  nchoicelem12  6300  nchoicelem17  6305  dmfrec  6316  fnfreclem2  6318  fnfreclem3  6319