Theorem pm2.21dd 623

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

This theorem is referenced by:  pm2.21fal  1415  pm2.21ddne  2483  ordtriexmidlem  4611  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  wetriext  4669  reg3exmidlemwe  4671  nntr2  6649  nnm00  6676  phpm  7027  fidifsnen  7032  dif1enen  7042  infnfi  7057  en2eqpr  7069  pr2cv1  7368  aptiprleml  7826  aptiprlemu  7827  uzdisj  10289  nn0disj  10334  zsupcllemex  10450  addmodlteq  10620  frec2uzlt2d  10626  iseqf1olemab  10724  iseqf1olemmo  10727  hashennnuni  11001  hashfiv01gt1  11004  xrmaxiflemab  11758  xrmaxiflemlub  11759  xrmaxltsup  11769  xrbdtri  11787  divalglemeunn  12432  divalglemeuneg  12434  ennnfonelemk  12971  cnplimclemle  15342  efltlemlt  15448  trilpolemlt1  16409  neapmkvlem  16435