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  7723  aptiprlemu  7724  uzdisj  10185  nn0disj  10230  zsupcllemex  10337  addmodlteq  10507  frec2uzlt2d  10513  iseqf1olemab  10611  iseqf1olemmo  10614  hashennnuni  10888  hashfiv01gt1  10891  xrmaxiflemab  11429  xrmaxiflemlub  11430  xrmaxltsup  11440  xrbdtri  11458  divalglemeunn  12103  divalglemeuneg  12105  ennnfonelemk  12642  cnplimclemle  14988  efltlemlt  15094  trilpolemlt1  15772  neapmkvlem  15798