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 )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 624

This theorem is referenced by:  pm2.21fal  1422  pm2.21ddne  2503  ordtriexmidlem  4664  ordtri2or2exmidlem  4671  onsucelsucexmidlem  4674  wetriext  4722  reg3exmidlemwe  4724  nntr2  6769  nnm00  6796  phpm  7160  fidifsnen  7165  dif1enen  7177  infnfi  7192  en2eqpr  7207  pr2cv1  7534  aptiprleml  7999  aptiprlemu  8000  uzdisj  10481  nn0disj  10526  zsupcllemex  10644  addmodlteq  10816  frec2uzlt2d  10822  iseqf1olemab  10920  iseqf1olemmo  10923  hashennnuni  11199  hashfiv01gt1  11202  xrmaxiflemab  11994  xrmaxiflemlub  11995  xrmaxltsup  12005  xrbdtri  12023  divalglemeunn  12669  divalglemeuneg  12671  ennnfonelemk  13272  cnplimclemle  15695  efltlemlt  15801  trilpolemlt1  16998  neapmkvlem  17025