ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.21dd Unicode version

Theorem pm2.21dd 585
Description: A contradiction implies anything. Deduction from pm2.21 582. (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 584 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mpd 13 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in2 580
This theorem is referenced by:  pm2.21fal  1309  pm2.21ddne  2338  ordtriexmidlem  4336  ordtri2or2exmidlem  4342  onsucelsucexmidlem  4345  wetriext  4392  reg3exmidlemwe  4394  nnm00  6286  phpm  6579  fidifsnen  6584  dif1enen  6594  infnfi  6609  en2eqpr  6621  aptiprleml  7196  aptiprlemu  7197  uzdisj  9503  nn0disj  9545  addmodlteq  9801  frec2uzlt2d  9807  iseqf1olemab  9914  iseqf1olemmo  9917  hashennnuni  10183  hashfiv01gt1  10186  divalglemeunn  11195  divalglemeuneg  11197  zsupcllemex  11216
  Copyright terms: Public domain W3C validator