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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.21fal  1591  pm2.21ddne  3039  smo11  8377  ackbij1lem16  10317  cfsmolem  10353  domtriomlem  10525  konigthlem  10658  grur1  10910  uzdisj  13736  nn0disj  13783  ccatf1  14741  sgnmul  15267  sgnmulsgn  15269  chnccats1  18806  chnccat  18807  psgnunilem2  19716  nmoleub2lem3  25443  i1f0  26015  itg2const2  26069  bposlem3  27620  bposlem9  27626  pntpbnd1  27920  infdesc  27974  prlngmolem2  29438  tgextahp  33080  tgextan  33086  sgnmulsgp  33471  fzto1st1  33711  cycpmco2lem5  33739  mxidlirred  34045  rprmdvdspow  34113  1arithufd  34128  0mplrim  34194  esumpcvgval  34758  signstfvneq0  35249  derangsn  36023  heiborlem8  38859  lkrpssN  40327  cdleme27a  41531  aks4d1p3  43235  aks4d1p5  43237  aks4d1p8  43244  primrootlekpowne0  43262  primrootspoweq0  43263  sticksstones22  43325  aks6d1c6lem3  43329  aks6d1c6lem4  43330  aks6d1c7lem2  43338  unitscyglem2  43353  unitscyglem4  43355  aks5lem8  43358  pellfundex  44000  monotoddzzfi  44056  jm2.23  44110  rp-isfinite6  44626  r1rankcld  45336  iccpartiltu  48611  iccpartigtl  48612  pgn4cyclex  49331