Theorem pm2.21dd 623

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

This theorem is referenced by:  pm2.21fal  1415  pm2.21ddne  2483  ordtriexmidlem  4610  ordtri2or2exmidlem  4617  onsucelsucexmidlem  4620  wetriext  4668  reg3exmidlemwe  4670  nntr2  6647  nnm00  6674  phpm  7023  fidifsnen  7028  dif1enen  7038  infnfi  7053  en2eqpr  7065  pr2cv1  7364  aptiprleml  7822  aptiprlemu  7823  uzdisj  10285  nn0disj  10330  zsupcllemex  10445  addmodlteq  10615  frec2uzlt2d  10621  iseqf1olemab  10719  iseqf1olemmo  10722  hashennnuni  10996  hashfiv01gt1  10999  xrmaxiflemab  11753  xrmaxiflemlub  11754  xrmaxltsup  11764  xrbdtri  11782  divalglemeunn  12427  divalglemeuneg  12429  ennnfonelemk  12966  cnplimclemle  15336  efltlemlt  15442  trilpolemlt1  16368  neapmkvlem  16394