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  4503  ordtri2or2exmidlem  4510  onsucelsucexmidlem  4513  wetriext  4561  reg3exmidlemwe  4563  nntr2  6482  nnm00  6509  phpm  6843  fidifsnen  6848  dif1enen  6858  infnfi  6873  en2eqpr  6885  aptiprleml  7601  aptiprlemu  7602  uzdisj  10049  nn0disj  10094  addmodlteq  10354  frec2uzlt2d  10360  iseqf1olemab  10445  iseqf1olemmo  10448  hashennnuni  10713  hashfiv01gt1  10716  xrmaxiflemab  11210  xrmaxiflemlub  11211  xrmaxltsup  11221  xrbdtri  11239  divalglemeunn  11880  divalglemeuneg  11882  zsupcllemex  11901  ennnfonelemk  12355  cnplimclemle  13431  efltlemlt  13489  trilpolemlt1  14073  neapmkvlem  14098
  Copyright terms: Public domain W3C validator