Theorem pm2.21dd 625

Description: A contradiction implies anything. Deduction from pm2.21 622. (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 624	. 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 620

This theorem is referenced by:  pm2.21fal  1418  pm2.21ddne  2486  ordtriexmidlem  4623  ordtri2or2exmidlem  4630  onsucelsucexmidlem  4633  wetriext  4681  reg3exmidlemwe  4683  nntr2  6714  nnm00  6741  phpm  7095  fidifsnen  7100  dif1enen  7112  infnfi  7127  en2eqpr  7142  pr2cv1  7443  aptiprleml  7902  aptiprlemu  7903  uzdisj  10373  nn0disj  10418  zsupcllemex  10536  addmodlteq  10706  frec2uzlt2d  10712  iseqf1olemab  10810  iseqf1olemmo  10813  hashennnuni  11087  hashfiv01gt1  11090  xrmaxiflemab  11870  xrmaxiflemlub  11871  xrmaxltsup  11881  xrbdtri  11899  divalglemeunn  12545  divalglemeuneg  12547  ennnfonelemk  13084  cnplimclemle  15462  efltlemlt  15568  trilpolemlt1  16756  neapmkvlem  16783