Theorem pm2.21dd 629

Description: A contradiction implies anything. Deduction from pm2.21 626. (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 628	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mpd 13	1 |- ( ph -> ch )

This proof depends on syntax axioms:   -. wn 3   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 624

This theorem is used by:  pm2.21fal  1422  pm2.21ddne  2503  ordtriexmidlem  4666  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  wetriext  4724  reg3exmidlemwe  4726  nntr2  6776  nnm00  6803  phpm  7167  fidifsnen  7172  dif1enen  7184  infnfi  7199  en2eqpr  7214  pr2cv1  7542  aptiprleml  8007  aptiprlemu  8008  uzdisj  10511  nn0disj  10556  zsupcllemex  10674  addmodlteq  10850  frec2uzlt2d  10856  iseqf1olemab  10954  iseqf1olemmo  10957  hashennnuni  11234  hashfiv01gt1  11237  xrmaxiflemab  12032  xrmaxiflemlub  12033  xrmaxltsup  12043  xrbdtri  12061  divalglemeunn  12707  divalglemeuneg  12709  ennnfonelemk  13343  cnplimclemle  15860  efltlemlt  15966  bposlem3  16274  bposlem9  16280  trilpolemlt1  17257  neapmkvlem  17284