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

Theorem pm2.21dd 592
Description: A contradiction implies anything. Deduction from pm2.21 589. (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 591 . 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 587
This theorem is referenced by:  pm2.21fal  1334  pm2.21ddne  2365  ordtriexmidlem  4395  ordtri2or2exmidlem  4401  onsucelsucexmidlem  4404  wetriext  4451  reg3exmidlemwe  4453  nntr2  6353  nnm00  6379  phpm  6712  fidifsnen  6717  dif1enen  6727  infnfi  6742  en2eqpr  6754  aptiprleml  7395  aptiprlemu  7396  uzdisj  9766  nn0disj  9808  addmodlteq  10064  frec2uzlt2d  10070  iseqf1olemab  10155  iseqf1olemmo  10158  hashennnuni  10418  hashfiv01gt1  10421  xrmaxiflemab  10908  xrmaxiflemlub  10909  xrmaxltsup  10919  xrbdtri  10937  divalglemeunn  11466  divalglemeuneg  11468  zsupcllemex  11487  ennnfonelemk  11758  cnplimclemle  12593  trilpolemlt1  12926
  Copyright terms: Public domain W3C validator