Theorem pm2.21dd 621

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

This theorem is referenced by:  pm2.21fal  1392  pm2.21ddne  2458  ordtriexmidlem  4566  ordtri2or2exmidlem  4573  onsucelsucexmidlem  4576  wetriext  4624  reg3exmidlemwe  4626  nntr2  6588  nnm00  6615  phpm  6961  fidifsnen  6966  dif1enen  6976  infnfi  6991  en2eqpr  7003  aptiprleml  7751  aptiprlemu  7752  uzdisj  10214  nn0disj  10259  zsupcllemex  10371  addmodlteq  10541  frec2uzlt2d  10547  iseqf1olemab  10645  iseqf1olemmo  10648  hashennnuni  10922  hashfiv01gt1  10925  xrmaxiflemab  11500  xrmaxiflemlub  11501  xrmaxltsup  11511  xrbdtri  11529  divalglemeunn  12174  divalglemeuneg  12176  ennnfonelemk  12713  cnplimclemle  15082  efltlemlt  15188  trilpolemlt1  15913  neapmkvlem  15939