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  1393  pm2.21ddne  2461  ordtriexmidlem  4585  ordtri2or2exmidlem  4592  onsucelsucexmidlem  4595  wetriext  4643  reg3exmidlemwe  4645  nntr2  6612  nnm00  6639  phpm  6988  fidifsnen  6993  dif1enen  7003  infnfi  7018  en2eqpr  7030  pr2cv1  7329  aptiprleml  7787  aptiprlemu  7788  uzdisj  10250  nn0disj  10295  zsupcllemex  10410  addmodlteq  10580  frec2uzlt2d  10586  iseqf1olemab  10684  iseqf1olemmo  10687  hashennnuni  10961  hashfiv01gt1  10964  xrmaxiflemab  11673  xrmaxiflemlub  11674  xrmaxltsup  11684  xrbdtri  11702  divalglemeunn  12347  divalglemeuneg  12349  ennnfonelemk  12886  cnplimclemle  15255  efltlemlt  15361  trilpolemlt1  16182  neapmkvlem  16208