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  1393  pm2.21ddne  2459  ordtriexmidlem  4567  ordtri2or2exmidlem  4574  onsucelsucexmidlem  4577  wetriext  4625  reg3exmidlemwe  4627  nntr2  6589  nnm00  6616  phpm  6962  fidifsnen  6967  dif1enen  6977  infnfi  6992  en2eqpr  7004  aptiprleml  7752  aptiprlemu  7753  uzdisj  10215  nn0disj  10260  zsupcllemex  10373  addmodlteq  10543  frec2uzlt2d  10549  iseqf1olemab  10647  iseqf1olemmo  10650  hashennnuni  10924  hashfiv01gt1  10927  xrmaxiflemab  11558  xrmaxiflemlub  11559  xrmaxltsup  11569  xrbdtri  11587  divalglemeunn  12232  divalglemeuneg  12234  ennnfonelemk  12771  cnplimclemle  15140  efltlemlt  15246  trilpolemlt1  15980  neapmkvlem  16006