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

Theorem pm2.21dd 615
Description: A contradiction implies anything. Deduction from pm2.21 612. (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 614 . 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 610
This theorem is referenced by:  pm2.21fal  1368  pm2.21ddne  2423  ordtriexmidlem  4501  ordtri2or2exmidlem  4508  onsucelsucexmidlem  4511  wetriext  4559  reg3exmidlemwe  4561  nntr2  6479  nnm00  6505  phpm  6839  fidifsnen  6844  dif1enen  6854  infnfi  6869  en2eqpr  6881  aptiprleml  7588  aptiprlemu  7589  uzdisj  10036  nn0disj  10081  addmodlteq  10341  frec2uzlt2d  10347  iseqf1olemab  10432  iseqf1olemmo  10435  hashennnuni  10700  hashfiv01gt1  10703  xrmaxiflemab  11197  xrmaxiflemlub  11198  xrmaxltsup  11208  xrbdtri  11226  divalglemeunn  11867  divalglemeuneg  11869  zsupcllemex  11888  ennnfonelemk  12342  cnplimclemle  13390  efltlemlt  13448  trilpolemlt1  14033  neapmkvlem  14058
  Copyright terms: Public domain W3C validator