Theorem pm2.21dd 623

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

This theorem is referenced by:  pm2.21fal  1415  pm2.21ddne  2483  ordtriexmidlem  4615  ordtri2or2exmidlem  4622  onsucelsucexmidlem  4625  wetriext  4673  reg3exmidlemwe  4675  nntr2  6666  nnm00  6693  phpm  7047  fidifsnen  7052  dif1enen  7062  infnfi  7077  en2eqpr  7092  pr2cv1  7391  aptiprleml  7849  aptiprlemu  7850  uzdisj  10318  nn0disj  10363  zsupcllemex  10480  addmodlteq  10650  frec2uzlt2d  10656  iseqf1olemab  10754  iseqf1olemmo  10757  hashennnuni  11031  hashfiv01gt1  11034  xrmaxiflemab  11798  xrmaxiflemlub  11799  xrmaxltsup  11809  xrbdtri  11827  divalglemeunn  12472  divalglemeuneg  12474  ennnfonelemk  13011  cnplimclemle  15382  efltlemlt  15488  trilpolemlt1  16581  neapmkvlem  16607