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

Theorem pm2.21dd 186
Description: A contradiction implies anything. Deduction from pm2.21 120. (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 185 . 2 ¬ 𝜑
43pm2.21i 116 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  1504  pm2.21ddne  2877  smo11  7458  ackbij1lem16  9054  cfsmolem  9089  domtriomlem  9261  konigthlem  9387  grur1  9639  uzdisj  12409  nn0disj  12451  psgnunilem2  17909  nmoleub2lem3  22909  i1f0  23448  itg2const2  23502  bposlem3  25005  bposlem9  25011  pntpbnd1  25269  fzto1st1  29837  esumpcvgval  30125  sgnmul  30589  sgnmulsgn  30596  sgnmulsgp  30597  signstfvneq0  30634  derangsn  31137  heiborlem8  33597  lkrpssN  34276  cdleme27a  35481  pellfundex  37276  monotoddzzfi  37333  jm2.23  37389  rp-isfinite6  37690  iccpartiltu  41128  iccpartigtl  41129
  Copyright terms: Public domain W3C validator