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

Theorem pm2.21dd 590
Description: A contradiction implies anything. Deduction from pm2.21 587. (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 589 . 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 585
This theorem is referenced by:  pm2.21fal  1319  pm2.21ddne  2350  ordtriexmidlem  4373  ordtri2or2exmidlem  4379  onsucelsucexmidlem  4382  wetriext  4429  reg3exmidlemwe  4431  nntr2  6329  nnm00  6355  phpm  6688  fidifsnen  6693  dif1enen  6703  infnfi  6718  en2eqpr  6730  aptiprleml  7348  aptiprlemu  7349  uzdisj  9714  nn0disj  9756  addmodlteq  10012  frec2uzlt2d  10018  iseqf1olemab  10103  iseqf1olemmo  10106  hashennnuni  10366  hashfiv01gt1  10369  xrmaxiflemab  10855  xrmaxiflemlub  10856  xrmaxltsup  10866  xrbdtri  10884  divalglemeunn  11413  divalglemeuneg  11415  zsupcllemex  11434  ennnfonelemk  11705  trilpolemlt1  12818
  Copyright terms: Public domain W3C validator