Theorem imim12iOLD 22

Description: Inference joining two implications.

Hypotheses

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

Assertion

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

Proof of Theorem imim12iOLD

Step	Hyp	Ref	Expression
1		imim12i.2	. . 3 |- (ch -> th)
2	1	imim2i 11	. 2 |- ((ps -> ch) -> (ps -> th))
3		imim12i.1	. . 3 |- (ph -> ps)
4	3	imim1i 19	. 2 |- ((ps -> th) -> (ph -> th))
5	2, 4	syl 12	1 |- ((ps -> ch) -> (ph -> th))

Syntax hints:   -> wi 3

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain