Theorem pm2.21dd 621

Description: A contradiction implies anything. Deduction from pm2.21 618. (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 620	. 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 616

This theorem is referenced by:  pm2.21fal  1384  pm2.21ddne  2447  ordtriexmidlem  4551  ordtri2or2exmidlem  4558  onsucelsucexmidlem  4561  wetriext  4609  reg3exmidlemwe  4611  nntr2  6556  nnm00  6583  phpm  6921  fidifsnen  6926  dif1enen  6936  infnfi  6951  en2eqpr  6963  aptiprleml  7699  aptiprlemu  7700  uzdisj  10159  nn0disj  10204  addmodlteq  10469  frec2uzlt2d  10475  iseqf1olemab  10573  iseqf1olemmo  10576  hashennnuni  10850  hashfiv01gt1  10853  xrmaxiflemab  11390  xrmaxiflemlub  11391  xrmaxltsup  11401  xrbdtri  11419  divalglemeunn  12062  divalglemeuneg  12064  zsupcllemex  12083  ennnfonelemk  12557  cnplimclemle  14822  efltlemlt  14909  trilpolemlt1  15531  neapmkvlem  15557