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

Theorem pm2.21dd 610
 Description: A contradiction implies anything. Deduction from pm2.21 607. (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 609 . 2 (𝜑 → (𝜓𝜒))
41, 3mpd 13 1 (𝜑𝜒)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 605 This theorem is referenced by:  pm2.21fal  1352  pm2.21ddne  2392  ordtriexmidlem  4442  ordtri2or2exmidlem  4448  onsucelsucexmidlem  4451  wetriext  4498  reg3exmidlemwe  4500  nntr2  6406  nnm00  6432  phpm  6766  fidifsnen  6771  dif1enen  6781  infnfi  6796  en2eqpr  6808  aptiprleml  7470  aptiprlemu  7471  uzdisj  9903  nn0disj  9945  addmodlteq  10201  frec2uzlt2d  10207  iseqf1olemab  10292  iseqf1olemmo  10295  hashennnuni  10556  hashfiv01gt1  10559  xrmaxiflemab  11047  xrmaxiflemlub  11048  xrmaxltsup  11058  xrbdtri  11076  divalglemeunn  11652  divalglemeuneg  11654  zsupcllemex  11673  ennnfonelemk  11947  cnplimclemle  12843  efltlemlt  12901  trilpolemlt1  13407  neapmkvlem  13422
 Copyright terms: Public domain W3C validator