Theorem pm2.21dd 629

Description: A contradiction implies anything. Deduction from pm2.21 626. (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 628	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 624

This theorem is used by:  pm2.21fal  1422  pm2.21ddne  2503  ordtriexmidlem  4666  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  wetriext  4724  reg3exmidlemwe  4726  nntr2  6776  nnm00  6803  phpm  7167  fidifsnen  7172  dif1enen  7184  infnfi  7199  en2eqpr  7214  pr2cv1  7541  aptiprleml  8006  aptiprlemu  8007  uzdisj  10510  nn0disj  10555  zsupcllemex  10673  addmodlteq  10848  frec2uzlt2d  10854  iseqf1olemab  10952  iseqf1olemmo  10955  hashennnuni  11232  hashfiv01gt1  11235  xrmaxiflemab  12029  xrmaxiflemlub  12030  xrmaxltsup  12040  xrbdtri  12058  divalglemeunn  12704  divalglemeuneg  12706  ennnfonelemk  13340  cnplimclemle  15818  efltlemlt  15924  bposlem3  16211  trilpolemlt1  17188  neapmkvlem  17215