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  1562  pm2.21ddne  3009  smo11  8294  ackbij1lem16  10147  cfsmolem  10183  domtriomlem  10355  konigthlem  10481  grur1  10733  uzdisj  13519  nn0disj  13566  psgnunilem2  19393  nmoleub2lem3  25032  i1f0  25605  itg2const2  25659  bposlem3  27214  bposlem9  27220  pntpbnd1  27514  sgnmul  32799  sgnmulsgn  32806  sgnmulsgp  32807  ccatf1  32909  chnccats1  32976  fzto1st1  33063  cycpmco2lem5  33091  mxidlirred  33428  rprmdvdspow  33489  1arithufd  33504  esumpcvgval  34064  signstfvneq0  34559  derangsn  35162  heiborlem8  37817  lkrpssN  39161  cdleme27a  40366  aks4d1p3  42071  aks4d1p5  42073  aks4d1p8  42080  primrootlekpowne0  42098  primrootspoweq0  42099  sticksstones22  42161  aks6d1c6lem3  42165  aks6d1c6lem4  42166  aks6d1c7lem2  42174  unitscyglem2  42189  unitscyglem4  42191  aks5lem8  42194  infdesc  42636  pellfundex  42879  monotoddzzfi  42935  jm2.23  42989  rp-isfinite6  43511  r1rankcld  44224  iccpartiltu  47426  iccpartigtl  47427  pgn4cyclex  48130