Theorem imim12i 18

Description: Inference joining two implications.

Hypotheses

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

Assertion

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

Proof of Theorem imim12i

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

Syntax hints:   -> wi 3

This theorem is referenced by:  pm5.75 751  dedlem0b 763  19.38 1083  exmoeu 1415  iununi 2621  pssnn 4544  kmlem1 4775  zorn 4807  brdom5 4812  brdom4 4813  axpowndlem2 4962  dfuz 6204  cau5i 6917

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

Copyright terms: Public domain