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	⊢ (𝜑 → 𝜓)
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 620	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝜒)

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  4556  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  wetriext  4614  reg3exmidlemwe  4616  nntr2  6570  nnm00  6597  phpm  6935  fidifsnen  6940  dif1enen  6950  infnfi  6965  en2eqpr  6977  aptiprleml  7725  aptiprlemu  7726  uzdisj  10187  nn0disj  10232  zsupcllemex  10339  addmodlteq  10509  frec2uzlt2d  10515  iseqf1olemab  10613  iseqf1olemmo  10616  hashennnuni  10890  hashfiv01gt1  10893  xrmaxiflemab  11431  xrmaxiflemlub  11432  xrmaxltsup  11442  xrbdtri  11460  divalglemeunn  12105  divalglemeuneg  12107  ennnfonelemk  12644  cnplimclemle  15012  efltlemlt  15118  trilpolemlt1  15798  neapmkvlem  15824