Theorem pm2.21dd 590

Description: A contradiction implies anything. Deduction from pm2.21 587. (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 589	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in2 585

This theorem is referenced by:  pm2.21fal  1319  pm2.21ddne  2350  ordtriexmidlem  4373  ordtri2or2exmidlem  4379  onsucelsucexmidlem  4382  wetriext  4429  reg3exmidlemwe  4431  nntr2  6329  nnm00  6355  phpm  6688  fidifsnen  6693  dif1enen  6703  infnfi  6718  en2eqpr  6730  aptiprleml  7348  aptiprlemu  7349  uzdisj  9714  nn0disj  9756  addmodlteq  10012  frec2uzlt2d  10018  iseqf1olemab  10103  iseqf1olemmo  10106  hashennnuni  10366  hashfiv01gt1  10369  xrmaxiflemab  10855  xrmaxiflemlub  10856  xrmaxltsup  10866  xrbdtri  10884  divalglemeunn  11413  divalglemeuneg  11415  zsupcllemex  11434  ennnfonelemk  11705  trilpolemlt1  12818