Theorem pm2.21dd 625

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

This theorem is referenced by:  pm2.21fal  1417  pm2.21ddne  2485  ordtriexmidlem  4617  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  wetriext  4675  reg3exmidlemwe  4677  nntr2  6674  nnm00  6701  phpm  7055  fidifsnen  7060  dif1enen  7072  infnfi  7087  en2eqpr  7102  pr2cv1  7403  aptiprleml  7862  aptiprlemu  7863  uzdisj  10331  nn0disj  10376  zsupcllemex  10494  addmodlteq  10664  frec2uzlt2d  10670  iseqf1olemab  10768  iseqf1olemmo  10771  hashennnuni  11045  hashfiv01gt1  11048  xrmaxiflemab  11828  xrmaxiflemlub  11829  xrmaxltsup  11839  xrbdtri  11857  divalglemeunn  12503  divalglemeuneg  12505  ennnfonelemk  13042  cnplimclemle  15419  efltlemlt  15525  trilpolemlt1  16704  neapmkvlem  16731