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  6670  nnm00  6697  phpm  7051  fidifsnen  7056  dif1enen  7068  infnfi  7083  en2eqpr  7098  pr2cv1  7399  aptiprleml  7858  aptiprlemu  7859  uzdisj  10327  nn0disj  10372  zsupcllemex  10489  addmodlteq  10659  frec2uzlt2d  10665  iseqf1olemab  10763  iseqf1olemmo  10766  hashennnuni  11040  hashfiv01gt1  11043  xrmaxiflemab  11807  xrmaxiflemlub  11808  xrmaxltsup  11818  xrbdtri  11836  divalglemeunn  12481  divalglemeuneg  12483  ennnfonelemk  13020  cnplimclemle  15391  efltlemlt  15497  trilpolemlt1  16645  neapmkvlem  16671