MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.21dd 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  1341  pm2.21ddne  2624  smo11  6562  ackbij1lem16  8048  cfsmolem  8083  domtriomlem  8255  konigthlem  8376  grur1  8628  uzdisj  11049  nmoleub2lem3  18994  i1f0  19446  itg2const2  19500  bposlem3  20937  bposlem9  20943  pntpbnd1  21147  esumpcvgval  24264  derangsn  24635  heiborlem8  26218  pellfundex  26640  monotoddzzfi  26696  jm2.23  26758  psgnunilem2  27087  lkrpssN  29278  cdleme27a  30481
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator