Theorem pm2.21dd 620

Description: A contradiction implies anything. Deduction from pm2.21 617. (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 619	. 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 615

This theorem is referenced by:  pm2.21fal  1373  pm2.21ddne  2430  ordtriexmidlem  4520  ordtri2or2exmidlem  4527  onsucelsucexmidlem  4530  wetriext  4578  reg3exmidlemwe  4580  nntr2  6507  nnm00  6534  phpm  6868  fidifsnen  6873  dif1enen  6883  infnfi  6898  en2eqpr  6910  aptiprleml  7641  aptiprlemu  7642  uzdisj  10096  nn0disj  10141  addmodlteq  10401  frec2uzlt2d  10407  iseqf1olemab  10492  iseqf1olemmo  10495  hashennnuni  10762  hashfiv01gt1  10765  xrmaxiflemab  11258  xrmaxiflemlub  11259  xrmaxltsup  11269  xrbdtri  11287  divalglemeunn  11929  divalglemeuneg  11931  zsupcllemex  11950  ennnfonelemk  12404  cnplimclemle  14277  efltlemlt  14335  trilpolemlt1  14930  neapmkvlem  14956