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

Theorem pm2.21dd 560
Description: A contradiction implies anything. Deduction from pm2.21 557. (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 559 . 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 555
This theorem is referenced by:  pm2.21fal  1280  pm2.21ddne  2303  ordtriexmidlem  4272  ordtri2or2exmidlem  4278  onsucelsucexmidlem  4281  wetriext  4328  reg3exmidlemwe  4330  nnm00  6132  phpm  6357  fidifsnen  6361  aptiprleml  6794  aptiprlemu  6795  uzdisj  9056  nn0disj  9096  addmodlteq  9347  frec2uzlt2d  9353  divalglemeunn  10232  divalglemeuneg  10234
  Copyright terms: Public domain W3C validator