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  4565  ordtri2or2exmidlem  4572  onsucelsucexmidlem  4575  wetriext  4623  reg3exmidlemwe  4625  nntr2  6579  nnm00  6606  phpm  6944  fidifsnen  6949  dif1enen  6959  infnfi  6974  en2eqpr  6986  aptiprleml  7734  aptiprlemu  7735  uzdisj  10197  nn0disj  10242  zsupcllemex  10354  addmodlteq  10524  frec2uzlt2d  10530  iseqf1olemab  10628  iseqf1olemmo  10631  hashennnuni  10905  hashfiv01gt1  10908  xrmaxiflemab  11477  xrmaxiflemlub  11478  xrmaxltsup  11488  xrbdtri  11506  divalglemeunn  12151  divalglemeuneg  12153  ennnfonelemk  12690  cnplimclemle  15058  efltlemlt  15164  trilpolemlt1  15844  neapmkvlem  15870