Theorem pm2.21dd 609

Description: A contradiction implies anything. Deduction from pm2.21 606. (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 608	. 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 604

This theorem is referenced by:  pm2.21fal  1351  pm2.21ddne  2391  ordtriexmidlem  4435  ordtri2or2exmidlem  4441  onsucelsucexmidlem  4444  wetriext  4491  reg3exmidlemwe  4493  nntr2  6399  nnm00  6425  phpm  6759  fidifsnen  6764  dif1enen  6774  infnfi  6789  en2eqpr  6801  aptiprleml  7447  aptiprlemu  7448  uzdisj  9873  nn0disj  9915  addmodlteq  10171  frec2uzlt2d  10177  iseqf1olemab  10262  iseqf1olemmo  10265  hashennnuni  10525  hashfiv01gt1  10528  xrmaxiflemab  11016  xrmaxiflemlub  11017  xrmaxltsup  11027  xrbdtri  11045  divalglemeunn  11618  divalglemeuneg  11620  zsupcllemex  11639  ennnfonelemk  11913  cnplimclemle  12806  trilpolemlt1  13234