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  1564  pm2.21ddne  3016  smo11  8304  ackbij1lem16  10156  cfsmolem  10192  domtriomlem  10364  konigthlem  10491  grur1  10743  uzdisj  13551  nn0disj  13598  chnccats1  18591  chnccat  18592  psgnunilem2  19470  nmoleub2lem3  25082  i1f0  25654  itg2const2  25708  bposlem3  27249  bposlem9  27255  pntpbnd1  27549  sgnmul  32908  sgnmulsgn  32915  sgnmulsgp  32916  ccatf1  33009  fzto1st1  33163  cycpmco2lem5  33191  mxidlirred  33532  rprmdvdspow  33593  1arithufd  33608  esumpcvgval  34222  signstfvneq0  34716  derangsn  35352  heiborlem8  38139  lkrpssN  39609  cdleme27a  40813  aks4d1p3  42517  aks4d1p5  42519  aks4d1p8  42526  primrootlekpowne0  42544  primrootspoweq0  42545  sticksstones22  42607  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c7lem2  42620  unitscyglem2  42635  unitscyglem4  42637  aks5lem8  42640  infdesc  43076  pellfundex  43314  monotoddzzfi  43370  jm2.23  43424  rp-isfinite6  43945  r1rankcld  44658  iccpartiltu  47882  iccpartigtl  47883  pgn4cyclex  48602