Theorem pm2.21dd 592

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

This theorem is referenced by:  pm2.21fal  1334  pm2.21ddne  2365  ordtriexmidlem  4395  ordtri2or2exmidlem  4401  onsucelsucexmidlem  4404  wetriext  4451  reg3exmidlemwe  4453  nntr2  6353  nnm00  6379  phpm  6712  fidifsnen  6717  dif1enen  6727  infnfi  6742  en2eqpr  6754  aptiprleml  7395  aptiprlemu  7396  uzdisj  9766  nn0disj  9808  addmodlteq  10064  frec2uzlt2d  10070  iseqf1olemab  10155  iseqf1olemmo  10158  hashennnuni  10418  hashfiv01gt1  10421  xrmaxiflemab  10908  xrmaxiflemlub  10909  xrmaxltsup  10919  xrbdtri  10937  divalglemeunn  11466  divalglemeuneg  11468  zsupcllemex  11487  ennnfonelemk  11758  cnplimclemle  12593  trilpolemlt1  12926