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

Theorem pm2.21dd 101
Description: A contradiction implies anything. Deduction from pm2.21 102. (Contributed by Mario Carneiro, 9-Feb-2017.)
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 . 2  |-  ( ph  ->  ps )
2 pm2.21dd.2 . . 3  |-  ( ph  ->  -.  ps )
32pm2.21d 100 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.21fal  1344  pm2.21ddne  2672  smo11  6618  ackbij1lem16  8107  cfsmolem  8142  domtriomlem  8314  konigthlem  8435  grur1  8687  uzdisj  11111  nmoleub2lem3  19115  i1f0  19571  itg2const2  19625  bposlem3  21062  bposlem9  21068  pntpbnd1  21272  esumpcvgval  24460  derangsn  24848  heiborlem8  26508  pellfundex  26930  monotoddzzfi  26986  jm2.23  27048  psgnunilem2  27376  lkrpssN  29888  cdleme27a  31091
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator