Theorem pm2.21dd

Description: A contradiction implies anything. Deduction from pm2.21 . (Contributed by Mario Carneiro, 9-Feb-2017) (Proof shortened by Wolf Lammen, 22-Jul-2019)

	Ref	Expression
Hypotheses	pm2.21dd.1	|- ( ph -> ps )
	pm2.21dd.2	|- ( ph -> -. ps )
Assertion	pm2.21dd	|- ( ph -> ch )

Proof

Step	Hyp	Ref	Expression
1		pm2.21dd.1	|- ( ph -> ps )
2		pm2.21dd.2	|- ( ph -> -. ps )
3	1 2	pm2.65i	|- -. ph
4	3	pm2.21i	|- ( ph -> ch )