Theorem pm2.21dd 625

Description: A contradiction implies anything. Deduction from pm2.21 622. (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 624	. 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-mp 5  ax-1 6  ax-2 7  ax-in2 620

This theorem is referenced by:  pm2.21fal  1418  pm2.21ddne  2486  ordtriexmidlem  4623  ordtri2or2exmidlem  4630  onsucelsucexmidlem  4633  wetriext  4681  reg3exmidlemwe  4683  nntr2  6714  nnm00  6741  phpm  7095  fidifsnen  7100  dif1enen  7112  infnfi  7127  en2eqpr  7142  pr2cv1  7460  aptiprleml  7919  aptiprlemu  7920  uzdisj  10390  nn0disj  10435  zsupcllemex  10553  addmodlteq  10723  frec2uzlt2d  10729  iseqf1olemab  10827  iseqf1olemmo  10830  hashennnuni  11104  hashfiv01gt1  11107  xrmaxiflemab  11887  xrmaxiflemlub  11888  xrmaxltsup  11898  xrbdtri  11916  divalglemeunn  12562  divalglemeuneg  12564  ennnfonelemk  13101  cnplimclemle  15479  efltlemlt  15585  trilpolemlt1  16773  neapmkvlem  16800