Theorem pm2.21dd 615

Description: A contradiction implies anything. Deduction from pm2.21 612. (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 614	. 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 610

This theorem is referenced by:  pm2.21fal  1368  pm2.21ddne  2423  ordtriexmidlem  4503  ordtri2or2exmidlem  4510  onsucelsucexmidlem  4513  wetriext  4561  reg3exmidlemwe  4563  nntr2  6482  nnm00  6509  phpm  6843  fidifsnen  6848  dif1enen  6858  infnfi  6873  en2eqpr  6885  aptiprleml  7601  aptiprlemu  7602  uzdisj  10049  nn0disj  10094  addmodlteq  10354  frec2uzlt2d  10360  iseqf1olemab  10445  iseqf1olemmo  10448  hashennnuni  10713  hashfiv01gt1  10716  xrmaxiflemab  11210  xrmaxiflemlub  11211  xrmaxltsup  11221  xrbdtri  11239  divalglemeunn  11880  divalglemeuneg  11882  zsupcllemex  11901  ennnfonelemk  12355  cnplimclemle  13431  efltlemlt  13489  trilpolemlt1  14073  neapmkvlem  14098