Theorem pm2.21dd 198

Description: A contradiction implies anything. Deduction from pm2.21 124. (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 196	. 2 ⊢ ¬ 𝜑
4	3	pm2.21i 120	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  1592  pm2.21ddne  3042  smo11  8347  ackbij1lem16  10213  cfsmolem  10249  domtriomlem  10421  konigthlem  10548  grur1  10800  uzdisj  13621  nn0disj  13668  sgnmul  15140  sgnmulsgn  15142  chnccats1  18676  chnccat  18677  psgnunilem2  19560  nmoleub2lem3  25274  i1f0  25846  itg2const2  25900  bposlem3  27450  bposlem9  27456  pntpbnd1  27750  prlngmolem2  29203  sgnmulsgp  33176  ccatf1  33269  fzto1st1  33422  cycpmco2lem5  33450  mxidlirred  33755  rprmdvdspow  33823  1arithufd  33838  0mplrim  33904  esumpcvgval  34468  signstfvneq0  34959  derangsn  35662  heiborlem8  38469  lkrpssN  39937  cdleme27a  41141  aks4d1p3  42845  aks4d1p5  42847  aks4d1p8  42854  primrootlekpowne0  42872  primrootspoweq0  42873  sticksstones22  42935  aks6d1c6lem3  42939  aks6d1c6lem4  42940  aks6d1c7lem2  42948  unitscyglem2  42963  unitscyglem4  42965  aks5lem8  42968  infdesc  43375  pellfundex  43613  monotoddzzfi  43669  jm2.23  43723  rp-isfinite6  44244  r1rankcld  44955  iccpartiltu  48171  iccpartigtl  48172  pgn4cyclex  48891