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

Theorem pm2.21dd 594
Description: A contradiction implies anything. Deduction from pm2.21 591. (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 593 . 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 589
This theorem is referenced by:  pm2.21fal  1336  pm2.21ddne  2368  ordtriexmidlem  4405  ordtri2or2exmidlem  4411  onsucelsucexmidlem  4414  wetriext  4461  reg3exmidlemwe  4463  nntr2  6367  nnm00  6393  phpm  6727  fidifsnen  6732  dif1enen  6742  infnfi  6757  en2eqpr  6769  aptiprleml  7415  aptiprlemu  7416  uzdisj  9841  nn0disj  9883  addmodlteq  10139  frec2uzlt2d  10145  iseqf1olemab  10230  iseqf1olemmo  10233  hashennnuni  10493  hashfiv01gt1  10496  xrmaxiflemab  10984  xrmaxiflemlub  10985  xrmaxltsup  10995  xrbdtri  11013  divalglemeunn  11545  divalglemeuneg  11547  zsupcllemex  11566  ennnfonelemk  11840  cnplimclemle  12733  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator