Theorem pm2.21dd 620

Description: A contradiction implies anything. Deduction from pm2.21 617. (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 619	. 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 615

This theorem is referenced by:  pm2.21fal  1373  pm2.21ddne  2430  ordtriexmidlem  4517  ordtri2or2exmidlem  4524  onsucelsucexmidlem  4527  wetriext  4575  reg3exmidlemwe  4577  nntr2  6500  nnm00  6527  phpm  6861  fidifsnen  6866  dif1enen  6876  infnfi  6891  en2eqpr  6903  aptiprleml  7634  aptiprlemu  7635  uzdisj  10087  nn0disj  10132  addmodlteq  10392  frec2uzlt2d  10398  iseqf1olemab  10483  iseqf1olemmo  10486  hashennnuni  10751  hashfiv01gt1  10754  xrmaxiflemab  11247  xrmaxiflemlub  11248  xrmaxltsup  11258  xrbdtri  11276  divalglemeunn  11917  divalglemeuneg  11919  zsupcllemex  11938  ennnfonelemk  12392  cnplimclemle  13999  efltlemlt  14057  trilpolemlt1  14640  neapmkvlem  14665