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  2495  ordtriexmidlem  4641  ordtri2or2exmidlem  4648  onsucelsucexmidlem  4651  wetriext  4699  reg3exmidlemwe  4701  nntr2  6736  nnm00  6763  phpm  7120  fidifsnen  7125  dif1enen  7137  infnfi  7152  en2eqpr  7167  pr2cv1  7492  aptiprleml  7954  aptiprlemu  7955  uzdisj  10427  nn0disj  10472  zsupcllemex  10590  addmodlteq  10760  frec2uzlt2d  10766  iseqf1olemab  10864  iseqf1olemmo  10867  hashennnuni  11142  hashfiv01gt1  11145  xrmaxiflemab  11932  xrmaxiflemlub  11933  xrmaxltsup  11943  xrbdtri  11961  divalglemeunn  12607  divalglemeuneg  12609  ennnfonelemk  13151  cnplimclemle  15533  efltlemlt  15639  trilpolemlt1  16825  trimul0or  16845  neapmkvlem  16853