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  4518  ordtri2or2exmidlem  4525  onsucelsucexmidlem  4528  wetriext  4576  reg3exmidlemwe  4578  nntr2  6503  nnm00  6530  phpm  6864  fidifsnen  6869  dif1enen  6879  infnfi  6894  en2eqpr  6906  aptiprleml  7637  aptiprlemu  7638  uzdisj  10092  nn0disj  10137  addmodlteq  10397  frec2uzlt2d  10403  iseqf1olemab  10488  iseqf1olemmo  10491  hashennnuni  10758  hashfiv01gt1  10761  xrmaxiflemab  11254  xrmaxiflemlub  11255  xrmaxltsup  11265  xrbdtri  11283  divalglemeunn  11925  divalglemeuneg  11927  zsupcllemex  11946  ennnfonelemk  12400  cnplimclemle  14107  efltlemlt  14165  trilpolemlt1  14759  neapmkvlem  14784
  Copyright terms: Public domain W3C validator