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

Theorem pm2.21dd 583
Description: A contradiction implies anything. Deduction from pm2.21 580. (Contributed by Mario Carneiro, 9-Feb-2017.)
Hypotheses
Ref Expression
pm2.21dd.1 (𝜑𝜓)
pm2.21dd.2 (𝜑 → ¬ 𝜓)
Assertion
Ref Expression
pm2.21dd (𝜑𝜒)

Proof of Theorem pm2.21dd
StepHypRef Expression
1 pm2.21dd.1 . 2 (𝜑𝜓)
2 pm2.21dd.2 . . 3 (𝜑 → ¬ 𝜓)
32pm2.21d 582 . 2 (𝜑 → (𝜓𝜒))
41, 3mpd 13 1 (𝜑𝜒)
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 578
This theorem is referenced by:  pm2.21fal  1305  pm2.21ddne  2332  ordtriexmidlem  4299  ordtri2or2exmidlem  4305  onsucelsucexmidlem  4308  wetriext  4355  reg3exmidlemwe  4357  nnm00  6218  phpm  6511  fidifsnen  6516  dif1enen  6526  infnfi  6541  en2eqpr  6550  aptiprleml  7101  aptiprlemu  7102  uzdisj  9400  nn0disj  9439  addmodlteq  9694  frec2uzlt2d  9700  hashennnuni  10022  hashfiv01gt1  10025  divalglemeunn  10701  divalglemeuneg  10703  zsupcllemex  10722
  Copyright terms: Public domain W3C validator