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  1393  pm2.21ddne  2460  ordtriexmidlem  4575  ordtri2or2exmidlem  4582  onsucelsucexmidlem  4585  wetriext  4633  reg3exmidlemwe  4635  nntr2  6602  nnm00  6629  phpm  6977  fidifsnen  6982  dif1enen  6992  infnfi  7007  en2eqpr  7019  aptiprleml  7772  aptiprlemu  7773  uzdisj  10235  nn0disj  10280  zsupcllemex  10395  addmodlteq  10565  frec2uzlt2d  10571  iseqf1olemab  10669  iseqf1olemmo  10672  hashennnuni  10946  hashfiv01gt1  10949  xrmaxiflemab  11633  xrmaxiflemlub  11634  xrmaxltsup  11644  xrbdtri  11662  divalglemeunn  12307  divalglemeuneg  12309  ennnfonelemk  12846  cnplimclemle  15215  efltlemlt  15321  trilpolemlt1  16121  neapmkvlem  16147