Theorem syl34d 29

Description: Deduction combining antecedents and consequents.

Hypotheses

Ref	Expression
syl34d.1	⊢ (φ → (ψ → χ))
syl34d.2	⊢ (φ → (θ → τ))

Assertion

Ref	Expression
syl34d	⊢ (φ → ((χ → θ) → (ψ → τ)))

Proof of Theorem syl34d

Step	Hyp	Ref	Expression
1		syl34d.1	. . 3 ⊢ (φ → (ψ → χ))
2	1	syl4d 28	. 2 ⊢ (φ → ((χ → θ) → (ψ → θ)))
3		syl34d.2	. . 3 ⊢ (φ → (θ → τ))
4	3	syl3d 26	. 2 ⊢ (φ → ((ψ → θ) → (ψ → τ)))
5	2, 4	syld 27	1 ⊢ (φ → ((χ → θ) → (ψ → τ)))

Syntax hints:   → wi 2

This theorem is referenced by:  pm3.48 430  mo 1020  peano5 2394  tfrlem1 2949  uzind 4603  dmdbr 5731

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org