Theorem pm2.21dd 582

Description: A contradiction implies anything. Deduction from pm2.21 579. (Contributed by Mario Carneiro, 9-Feb-2017.)

Hypotheses

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

Assertion

Ref	Expression
pm2.21dd	|- ( ph -> ch )

Proof of Theorem pm2.21dd

Step	Hyp	Ref	Expression
1		pm2.21dd.1	. 2 |- ( ph -> ps )
2		pm2.21dd.2	. . 3 |- ( ph -> -. ps )
3	2	pm2.21d 581	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mpd 13	1 |- ( ph -> ch )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in2 577

This theorem is referenced by:  pm2.21fal  1304  pm2.21ddne  2328  ordtriexmidlem  4263  ordtri2or2exmidlem  4269  onsucelsucexmidlem  4272  wetriext  4319  reg3exmidlemwe  4321  nnm00  6125  phpm  6351  fidifsnen  6355  en2eqpr  6380  aptiprleml  6829  aptiprlemu  6830  uzdisj  9110  nn0disj  9148  addmodlteq  9400  frec2uzlt2d  9406  divalglemeunn  10321  divalglemeuneg  10323  zsupcllemex  10342