Theorem pm2.21dd 629

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

This theorem is referenced by:  pm2.21fal  1422  pm2.21ddne  2503  ordtriexmidlem  4661  ordtri2or2exmidlem  4668  onsucelsucexmidlem  4671  wetriext  4719  reg3exmidlemwe  4721  nntr2  6766  nnm00  6793  phpm  7157  fidifsnen  7162  dif1enen  7174  infnfi  7189  en2eqpr  7204  pr2cv1  7531  aptiprleml  7996  aptiprlemu  7997  uzdisj  10478  nn0disj  10523  zsupcllemex  10641  addmodlteq  10813  frec2uzlt2d  10819  iseqf1olemab  10917  iseqf1olemmo  10920  hashennnuni  11196  hashfiv01gt1  11199  xrmaxiflemab  11991  xrmaxiflemlub  11992  xrmaxltsup  12002  xrbdtri  12020  divalglemeunn  12666  divalglemeuneg  12668  ennnfonelemk  13269  cnplimclemle  15692  efltlemlt  15798  trilpolemlt1  16995  neapmkvlem  17022