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	⊢ (𝜑 → 𝜓)
pm2.21dd.2	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
pm2.21dd	⊢ (𝜑 → 𝜒)

Proof of Theorem pm2.21dd

Step	Hyp	Ref	Expression
1		pm2.21dd.1	. 2 ⊢ (𝜑 → 𝜓)
2		pm2.21dd.2	. . 3 ⊢ (𝜑 → ¬ 𝜓)
3	2	pm2.21d 628	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝜒)

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  sn0disj  4127  ordtriexmidlem  4668  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  wetriext  4726  reg3exmidlemwe  4728  nntr2  6781  nnm00  6808  phpm  7173  fidifsnen  7178  dif1enen  7190  infnfi  7205  en2eqpr  7220  pr2cv1  7547  aptiprleml  8012  aptiprlemu  8013  uzdisj  10516  nn0disj  10561  zsupcllemex  10679  addmodlteq  10855  frec2uzlt2d  10861  iseqf1olemab  10959  iseqf1olemmo  10962  hashennnuni  11239  hashfiv01gt1  11242  xrmaxiflemab  12037  xrmaxiflemlub  12038  xrmaxltsup  12048  xrbdtri  12066  divalglemeunn  12712  divalglemeuneg  12714  ennnfonelemk  13348  cnplimclemle  15911  efltlemlt  16017  bposlem3  16330  bposlem9  16336  trilpolemlt1  17314  neapmkvlem  17341