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  2497  ordtriexmidlem  4646  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  wetriext  4704  reg3exmidlemwe  4706  nntr2  6749  nnm00  6776  phpm  7133  fidifsnen  7138  dif1enen  7150  infnfi  7165  en2eqpr  7180  pr2cv1  7505  aptiprleml  7970  aptiprlemu  7971  uzdisj  10449  nn0disj  10494  zsupcllemex  10612  addmodlteq  10784  frec2uzlt2d  10790  iseqf1olemab  10888  iseqf1olemmo  10891  hashennnuni  11167  hashfiv01gt1  11170  xrmaxiflemab  11957  xrmaxiflemlub  11958  xrmaxltsup  11968  xrbdtri  11986  divalglemeunn  12632  divalglemeuneg  12634  ennnfonelemk  13235  cnplimclemle  15659  efltlemlt  15765  trilpolemlt1  16951  trimul0or  16971  neapmkvlem  16979