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  10500  nn0disj  10545  zsupcllemex  10663  addmodlteq  10835  frec2uzlt2d  10841  iseqf1olemab  10939  iseqf1olemmo  10942  hashennnuni  11218  hashfiv01gt1  11221  xrmaxiflemab  12013  xrmaxiflemlub  12014  xrmaxltsup  12024  xrbdtri  12042  divalglemeunn  12688  divalglemeuneg  12690  ennnfonelemk  13291  cnplimclemle  15769  efltlemlt  15875  trilpolemlt1  17090  neapmkvlem  17117