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  6657  nnm00  6684  phpm  7035  fidifsnen  7040  dif1enen  7050  infnfi  7065  en2eqpr  7080  pr2cv1  7379  aptiprleml  7837  aptiprlemu  7838  uzdisj  10301  nn0disj  10346  zsupcllemex  10462  addmodlteq  10632  frec2uzlt2d  10638  iseqf1olemab  10736  iseqf1olemmo  10739  hashennnuni  11013  hashfiv01gt1  11016  xrmaxiflemab  11774  xrmaxiflemlub  11775  xrmaxltsup  11785  xrbdtri  11803  divalglemeunn  12448  divalglemeuneg  12450  ennnfonelemk  12987  cnplimclemle  15358  efltlemlt  15464  trilpolemlt1  16497  neapmkvlem  16523