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  4647  ordtri2or2exmidlem  4654  onsucelsucexmidlem  4657  wetriext  4705  reg3exmidlemwe  4707  nntr2  6750  nnm00  6777  phpm  7134  fidifsnen  7139  dif1enen  7151  infnfi  7166  en2eqpr  7181  pr2cv1  7506  aptiprleml  7971  aptiprlemu  7972  uzdisj  10453  nn0disj  10498  zsupcllemex  10616  addmodlteq  10788  frec2uzlt2d  10794  iseqf1olemab  10892  iseqf1olemmo  10895  hashennnuni  11171  hashfiv01gt1  11174  xrmaxiflemab  11962  xrmaxiflemlub  11963  xrmaxltsup  11973  xrbdtri  11991  divalglemeunn  12637  divalglemeuneg  12639  ennnfonelemk  13240  cnplimclemle  15664  efltlemlt  15770  trilpolemlt1  16966  neapmkvlem  16993