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  4501  ordtri2or2exmidlem  4508  onsucelsucexmidlem  4511  wetriext  4559  reg3exmidlemwe  4561  nntr2  6480  nnm00  6507  phpm  6841  fidifsnen  6846  dif1enen  6856  infnfi  6871  en2eqpr  6883  aptiprleml  7594  aptiprlemu  7595  uzdisj  10042  nn0disj  10087  addmodlteq  10347  frec2uzlt2d  10353  iseqf1olemab  10438  iseqf1olemmo  10441  hashennnuni  10706  hashfiv01gt1  10709  xrmaxiflemab  11203  xrmaxiflemlub  11204  xrmaxltsup  11214  xrbdtri  11232  divalglemeunn  11873  divalglemeuneg  11875  zsupcllemex  11894  ennnfonelemk  12348  cnplimclemle  13396  efltlemlt  13454  trilpolemlt1  14038  neapmkvlem  14063