Theorem pm2.21dd 610

Description: A contradiction implies anything. Deduction from pm2.21 607. (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 609	. 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 605

This theorem is referenced by:  pm2.21fal  1362  pm2.21ddne  2417  ordtriexmidlem  4490  ordtri2or2exmidlem  4497  onsucelsucexmidlem  4500  wetriext  4548  reg3exmidlemwe  4550  nntr2  6462  nnm00  6488  phpm  6822  fidifsnen  6827  dif1enen  6837  infnfi  6852  en2eqpr  6864  aptiprleml  7571  aptiprlemu  7572  uzdisj  10018  nn0disj  10063  addmodlteq  10323  frec2uzlt2d  10329  iseqf1olemab  10414  iseqf1olemmo  10417  hashennnuni  10681  hashfiv01gt1  10684  xrmaxiflemab  11174  xrmaxiflemlub  11175  xrmaxltsup  11185  xrbdtri  11203  divalglemeunn  11843  divalglemeuneg  11845  zsupcllemex  11864  ennnfonelemk  12270  cnplimclemle  13178  efltlemlt  13236  trilpolemlt1  13754  neapmkvlem  13779