Theorem pm2.21dd 195

Description: A contradiction implies anything. Deduction from pm2.21 123. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 22-Jul-2019.)

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	. . 3 ⊢ (𝜑 → 𝜓)
2		pm2.21dd.2	. . 3 ⊢ (𝜑 → ¬ 𝜓)
3	1, 2	pm2.65i 194	. 2 ⊢ ¬ 𝜑
4	3	pm2.21i 119	1 ⊢ (𝜑 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.21fal  1563  pm2.21ddne  3013  smo11  8293  ackbij1lem16  10136  cfsmolem  10172  domtriomlem  10344  konigthlem  10470  grur1  10722  uzdisj  13504  nn0disj  13551  chnccats1  18539  chnccat  18540  psgnunilem2  19415  nmoleub2lem3  25062  i1f0  25635  itg2const2  25689  bposlem3  27244  bposlem9  27250  pntpbnd1  27544  sgnmul  32844  sgnmulsgn  32851  sgnmulsgp  32852  ccatf1  32959  fzto1st1  33112  cycpmco2lem5  33140  mxidlirred  33481  rprmdvdspow  33542  1arithufd  33557  esumpcvgval  34163  signstfvneq0  34657  derangsn  35286  heiborlem8  37931  lkrpssN  39335  cdleme27a  40539  aks4d1p3  42244  aks4d1p5  42246  aks4d1p8  42253  primrootlekpowne0  42271  primrootspoweq0  42272  sticksstones22  42334  aks6d1c6lem3  42338  aks6d1c6lem4  42339  aks6d1c7lem2  42347  unitscyglem2  42362  unitscyglem4  42364  aks5lem8  42367  infdesc  42801  pellfundex  43043  monotoddzzfi  43099  jm2.23  43153  rp-isfinite6  43675  r1rankcld  44388  iccpartiltu  47584  iccpartigtl  47585  pgn4cyclex  48288