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  2497  ordtriexmidlem  4643  ordtri2or2exmidlem  4650  onsucelsucexmidlem  4653  wetriext  4701  reg3exmidlemwe  4703  nntr2  6738  nnm00  6765  phpm  7122  fidifsnen  7127  dif1enen  7139  infnfi  7154  en2eqpr  7169  pr2cv1  7494  aptiprleml  7956  aptiprlemu  7957  uzdisj  10431  nn0disj  10476  zsupcllemex  10594  addmodlteq  10764  frec2uzlt2d  10770  iseqf1olemab  10868  iseqf1olemmo  10871  hashennnuni  11146  hashfiv01gt1  11149  xrmaxiflemab  11936  xrmaxiflemlub  11937  xrmaxltsup  11947  xrbdtri  11965  divalglemeunn  12611  divalglemeuneg  12613  ennnfonelemk  13168  cnplimclemle  15550  efltlemlt  15656  trilpolemlt1  16842  trimul0or  16862  neapmkvlem  16870