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  1384  pm2.21ddne  2447  ordtriexmidlem  4552  ordtri2or2exmidlem  4559  onsucelsucexmidlem  4562  wetriext  4610  reg3exmidlemwe  4612  nntr2  6558  nnm00  6585  phpm  6923  fidifsnen  6928  dif1enen  6938  infnfi  6953  en2eqpr  6965  aptiprleml  7701  aptiprlemu  7702  uzdisj  10162  nn0disj  10207  addmodlteq  10472  frec2uzlt2d  10478  iseqf1olemab  10576  iseqf1olemmo  10579  hashennnuni  10853  hashfiv01gt1  10856  xrmaxiflemab  11393  xrmaxiflemlub  11394  xrmaxltsup  11404  xrbdtri  11422  divalglemeunn  12065  divalglemeuneg  12067  zsupcllemex  12086  ennnfonelemk  12560  cnplimclemle  14847  efltlemlt  14950  trilpolemlt1  15601  neapmkvlem  15627