MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.21dd Structured version   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  |-  ( ph  ->  ps )
pm2.21dd.2  |-  ( ph  ->  -.  ps )
Assertion
Ref Expression
pm2.21dd  |-  ( ph  ->  ch )

Proof of Theorem pm2.21dd
StepHypRef Expression
1 pm2.21dd.1 . . 3  |-  ( ph  ->  ps )
2 pm2.21dd.2 . . 3  |-  ( ph  ->  -.  ps )
31, 2pm2.65i 173 . 2  |-  -.  ph
43pm2.21i 131 1  |-  ( ph  ->  ch )
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  1402  pm2.21ddne  2781  smo11  7035  ackbij1lem16  8615  cfsmolem  8650  domtriomlem  8822  konigthlem  8943  grur1  9198  uzdisj  11751  nn0disj  11788  psgnunilem2  16326  nmoleub2lem3  21361  i1f0  21857  itg2const2  21911  bposlem3  23317  bposlem9  23323  pntpbnd1  23527  archiabllem2c  27429  esumpcvgval  27752  sgnmul  28149  sgnsub  28151  sgnmulsgn  28156  sgnmulsgp  28157  signstfvneq0  28197  derangsn  28282  heiborlem8  29945  negel  30136  pellfundex  30454  monotoddzzfi  30510  jm2.23  30570  lkrpssN  33978  cdleme27a  35181
  Copyright terms: Public domain W3C validator