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  1417  pm2.21ddne  2485  ordtriexmidlem  4617  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  wetriext  4675  reg3exmidlemwe  4677  nntr2  6671  nnm00  6698  phpm  7052  fidifsnen  7057  dif1enen  7069  infnfi  7084  en2eqpr  7099  pr2cv1  7400  aptiprleml  7859  aptiprlemu  7860  uzdisj  10328  nn0disj  10373  zsupcllemex  10491  addmodlteq  10661  frec2uzlt2d  10667  iseqf1olemab  10765  iseqf1olemmo  10768  hashennnuni  11042  hashfiv01gt1  11045  xrmaxiflemab  11812  xrmaxiflemlub  11813  xrmaxltsup  11823  xrbdtri  11841  divalglemeunn  12487  divalglemeuneg  12489  ennnfonelemk  13026  cnplimclemle  15398  efltlemlt  15504  trilpolemlt1  16671  neapmkvlem  16698