Theorem pm2.21dd 620

Description: A contradiction implies anything. Deduction from pm2.21 617. (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 619	. 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 615

This theorem is referenced by:  pm2.21fal  1373  pm2.21ddne  2430  ordtriexmidlem  4519  ordtri2or2exmidlem  4526  onsucelsucexmidlem  4529  wetriext  4577  reg3exmidlemwe  4579  nntr2  6504  nnm00  6531  phpm  6865  fidifsnen  6870  dif1enen  6880  infnfi  6895  en2eqpr  6907  aptiprleml  7638  aptiprlemu  7639  uzdisj  10093  nn0disj  10138  addmodlteq  10398  frec2uzlt2d  10404  iseqf1olemab  10489  iseqf1olemmo  10492  hashennnuni  10759  hashfiv01gt1  10762  xrmaxiflemab  11255  xrmaxiflemlub  11256  xrmaxltsup  11266  xrbdtri  11284  divalglemeunn  11926  divalglemeuneg  11928  zsupcllemex  11947  ennnfonelemk  12401  cnplimclemle  14140  efltlemlt  14198  trilpolemlt1  14792  neapmkvlem  14817