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  2389  ordtriexmidlem  4430  ordtri2or2exmidlem  4436  onsucelsucexmidlem  4439  wetriext  4486  reg3exmidlemwe  4488  nntr2  6392  nnm00  6418  phpm  6752  fidifsnen  6757  dif1enen  6767  infnfi  6782  en2eqpr  6794  aptiprleml  7440  aptiprlemu  7441  uzdisj  9866  nn0disj  9908  addmodlteq  10164  frec2uzlt2d  10170  iseqf1olemab  10255  iseqf1olemmo  10258  hashennnuni  10518  hashfiv01gt1  10521  xrmaxiflemab  11009  xrmaxiflemlub  11010  xrmaxltsup  11020  xrbdtri  11038  divalglemeunn  11607  divalglemeuneg  11609  zsupcllemex  11628  ennnfonelemk  11902  cnplimclemle  12795  trilpolemlt1  13223