Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.21dd Structured version   Visualization version   GIF version

Theorem pm2.21dd 197
 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
StepHypRef Expression
1 pm2.21dd.1 . . 3 (𝜑𝜓)
2 pm2.21dd.2 . . 3 (𝜑 → ¬ 𝜓)
31, 2pm2.65i 196 . 2 ¬ 𝜑
43pm2.21i 119 1 (𝜑𝜒)
 Colors of variables: wff setvar class 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  1555  pm2.21ddne  3101  smo11  7995  ackbij1lem16  9651  cfsmolem  9686  domtriomlem  9858  konigthlem  9984  grur1  10236  uzdisj  12974  nn0disj  13017  psgnunilem2  18617  nmoleub2lem3  23713  i1f0  24282  itg2const2  24336  bposlem3  25856  bposlem9  25862  pntpbnd1  26156  ccatf1  30620  fzto1st1  30739  cycpmco2lem5  30767  esumpcvgval  31332  sgnmul  31795  sgnmulsgn  31802  sgnmulsgp  31803  signstfvneq0  31837  derangsn  32412  heiborlem8  35090  lkrpssN  36293  cdleme27a  37497  pellfundex  39476  monotoddzzfi  39532  jm2.23  39586  rp-isfinite6  39877  r1rankcld  40560  iccpartiltu  43575  iccpartigtl  43576
 Copyright terms: Public domain W3C validator