Theorem pm2.21dd 629

Description: A contradiction implies anything. Deduction from pm2.21 626. (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 628	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mpd 13	1 |- ( ph -> ch )

This proof depends on syntax axioms:   -. wn 3   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 624

This theorem is used by:  pm2.21fal  1422  pm2.21ddne  2503  sn0disj  4127  ordtriexmidlem  4668  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  wetriext  4726  reg3exmidlemwe  4728  nntr2  6780  nnm00  6807  phpm  7171  fidifsnen  7176  dif1enen  7188  infnfi  7203  en2eqpr  7218  pr2cv1  7547  aptiprleml  8012  aptiprlemu  8013  uzdisj  10517  nn0disj  10562  zsupcllemex  10680  addmodlteq  10856  frec2uzlt2d  10862  iseqf1olemab  10960  iseqf1olemmo  10963  hashennnuni  11240  hashfiv01gt1  11243  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxltsup  12049  xrbdtri  12067  divalglemeunn  12713  divalglemeuneg  12715  ennnfonelemk  13349  cnplimclemle  15894  efltlemlt  16000  bposlem3  16313  bposlem9  16319  trilpolemlt1  17297  neapmkvlem  17324