Theorem pm2.21dd 610

Description: A contradiction implies anything. Deduction from pm2.21 607. (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 609	. 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 605

This theorem is referenced by:  pm2.21fal  1363  pm2.21ddne  2419  ordtriexmidlem  4496  ordtri2or2exmidlem  4503  onsucelsucexmidlem  4506  wetriext  4554  reg3exmidlemwe  4556  nntr2  6471  nnm00  6497  phpm  6831  fidifsnen  6836  dif1enen  6846  infnfi  6861  en2eqpr  6873  aptiprleml  7580  aptiprlemu  7581  uzdisj  10028  nn0disj  10073  addmodlteq  10333  frec2uzlt2d  10339  iseqf1olemab  10424  iseqf1olemmo  10427  hashennnuni  10692  hashfiv01gt1  10695  xrmaxiflemab  11188  xrmaxiflemlub  11189  xrmaxltsup  11199  xrbdtri  11217  divalglemeunn  11858  divalglemeuneg  11860  zsupcllemex  11879  ennnfonelemk  12333  cnplimclemle  13277  efltlemlt  13335  trilpolemlt1  13920  neapmkvlem  13945