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

Theorem pm2.21dd 174
Description: A contradiction implies anything. Deduction from pm2.21 108. (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 173 . 2
43pm2.21i 131 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  pm2.21fal  1418  pm2.21ddne  2771  smo11  7054  ackbij1lem16  8636  cfsmolem  8671  domtriomlem  8843  konigthlem  8964  grur1  9219  uzdisj  11780  nn0disj  11820  psgnunilem2  16520  nmoleub2lem3  21598  i1f0  22094  itg2const2  22148  bposlem3  23561  bposlem9  23567  pntpbnd1  23771  esumpcvgval  28084  sgnmul  28481  sgnmulsgn  28488  sgnmulsgp  28489  signstfvneq0  28529  derangsn  28614  heiborlem8  30314  pellfundex  30822  monotoddzzfi  30878  jm2.23  30938  lkrpssN  34888  cdleme27a  36093  rp-isfinite6  37744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator