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

Theorem pm2.21dd 620
Description: A contradiction implies anything. Deduction from pm2.21 617. (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 619 . 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 615
This theorem is referenced by:  pm2.21fal  1373  pm2.21ddne  2430  ordtriexmidlem  4520  ordtri2or2exmidlem  4527  onsucelsucexmidlem  4530  wetriext  4578  reg3exmidlemwe  4580  nntr2  6506  nnm00  6533  phpm  6867  fidifsnen  6872  dif1enen  6882  infnfi  6897  en2eqpr  6909  aptiprleml  7640  aptiprlemu  7641  uzdisj  10095  nn0disj  10140  addmodlteq  10400  frec2uzlt2d  10406  iseqf1olemab  10491  iseqf1olemmo  10494  hashennnuni  10761  hashfiv01gt1  10764  xrmaxiflemab  11257  xrmaxiflemlub  11258  xrmaxltsup  11268  xrbdtri  11286  divalglemeunn  11928  divalglemeuneg  11930  zsupcllemex  11949  ennnfonelemk  12403  cnplimclemle  14222  efltlemlt  14280  trilpolemlt1  14874  neapmkvlem  14900
  Copyright terms: Public domain W3C validator