Theorem pm2.21dd 621

Description: A contradiction implies anything. Deduction from pm2.21 618. (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 620	. 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 616

This theorem is referenced by:  pm2.21fal  1384  pm2.21ddne  2450  ordtriexmidlem  4555  ordtri2or2exmidlem  4562  onsucelsucexmidlem  4565  wetriext  4613  reg3exmidlemwe  4615  nntr2  6561  nnm00  6588  phpm  6926  fidifsnen  6931  dif1enen  6941  infnfi  6956  en2eqpr  6968  aptiprleml  7706  aptiprlemu  7707  uzdisj  10168  nn0disj  10213  zsupcllemex  10320  addmodlteq  10490  frec2uzlt2d  10496  iseqf1olemab  10594  iseqf1olemmo  10597  hashennnuni  10871  hashfiv01gt1  10874  xrmaxiflemab  11412  xrmaxiflemlub  11413  xrmaxltsup  11423  xrbdtri  11441  divalglemeunn  12086  divalglemeuneg  12088  ennnfonelemk  12617  cnplimclemle  14904  efltlemlt  15010  trilpolemlt1  15685  neapmkvlem  15711