Theorem pm2.21dd 615

Description: A contradiction implies anything. Deduction from pm2.21 612. (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 614	. 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 610

This theorem is referenced by:  pm2.21fal  1368  pm2.21ddne  2423  ordtriexmidlem  4501  ordtri2or2exmidlem  4508  onsucelsucexmidlem  4511  wetriext  4559  reg3exmidlemwe  4561  nntr2  6479  nnm00  6505  phpm  6839  fidifsnen  6844  dif1enen  6854  infnfi  6869  en2eqpr  6881  aptiprleml  7588  aptiprlemu  7589  uzdisj  10036  nn0disj  10081  addmodlteq  10341  frec2uzlt2d  10347  iseqf1olemab  10432  iseqf1olemmo  10435  hashennnuni  10700  hashfiv01gt1  10703  xrmaxiflemab  11197  xrmaxiflemlub  11198  xrmaxltsup  11208  xrbdtri  11226  divalglemeunn  11867  divalglemeuneg  11869  zsupcllemex  11888  ennnfonelemk  12342  cnplimclemle  13390  efltlemlt  13448  trilpolemlt1  14033  neapmkvlem  14058