Theorem contrd

Description: A proof by contradiction, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018)

	Ref	Expression
Hypotheses	contrd.1	|- ( ph -> ( -. ps -> ch ) )
	contrd.2	|- ( ph -> ( -. ps -> -. ch ) )
Assertion	contrd	|- ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		contrd.1	|- ( ph -> ( -. ps -> ch ) )
2		contrd.2	|- ( ph -> ( -. ps -> -. ch ) )
3	1 2	jcad	|- ( ph -> ( -. ps -> ( ch /\ -. ch ) ) )
4		pm2.24	|- ( ch -> ( -. ch -> ps ) )
5	4	imp	|- ( ( ch /\ -. ch ) -> ps )
6	5	imim2i	|- ( ( -. ps -> ( ch /\ -. ch ) ) -> ( -. ps -> ps ) )
7	6	pm2.18d	|- ( ( -. ps -> ( ch /\ -. ch ) ) -> ps )
8	3 7	syl	|- ( ph -> ps )