Theorem syl34 20

Description: Inference joining two implications.

Hypotheses

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

Assertion

Ref	Expression
syl34	⊢ ((ψ → χ) → (φ → θ))

Proof of Theorem syl34

Step	Hyp	Ref	Expression
1		syl34.2	. . 3 ⊢ (χ → θ)
2	1	syl3 18	. 2 ⊢ ((ψ → χ) → (ψ → θ))
3		syl34.1	. . 3 ⊢ (φ → ψ)
4	3	syl4 19	. 2 ⊢ ((ψ → θ) → (φ → θ))
5	2, 4	syl 12	1 ⊢ ((ψ → χ) → (φ → θ))

Syntax hints:   → wi 2

This theorem is referenced by:  dedlem0b 568  19.38 760  exmoeu 1039  iununi 2037  pssnn 3428  kmlem1 3580  zorn2 3612  axpowndlem2 3744

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

metamath.org