Theorem syl34 20

Description: Inference joining two implications.

Hypotheses

Ref	Expression
syl34.1	|- (ph -> ps)
syl34.2	|- (ch -> th)

Assertion

Ref	Expression
syl34	|- ((ps -> ch) -> (ph -> th))

Proof of Theorem syl34

Step	Hyp	Ref	Expression
1		syl34.2	. . 3 |- (ch -> th)
2	1	syl3 18	. 2 |- ((ps -> ch) -> (ps -> th))
3		syl34.1	. . 3 |- (ph -> ps)
4	3	syl4 19	. 2 |- ((ps -> th) -> (ph -> th))
5	2, 4	syl 12	1 |- ((ps -> ch) -> (ph -> th))

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