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  4611  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  wetriext  4669  reg3exmidlemwe  4671  nntr2  6657  nnm00  6684  phpm  7035  fidifsnen  7040  dif1enen  7050  infnfi  7065  en2eqpr  7080  pr2cv1  7379  aptiprleml  7837  aptiprlemu  7838  uzdisj  10301  nn0disj  10346  zsupcllemex  10462  addmodlteq  10632  frec2uzlt2d  10638  iseqf1olemab  10736  iseqf1olemmo  10739  hashennnuni  11013  hashfiv01gt1  11016  xrmaxiflemab  11773  xrmaxiflemlub  11774  xrmaxltsup  11784  xrbdtri  11802  divalglemeunn  12447  divalglemeuneg  12449  ennnfonelemk  12986  cnplimclemle  15357  efltlemlt  15463  trilpolemlt1  16469  neapmkvlem  16495