Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm2.21dd | GIF version |
Description: A contradiction implies anything. Deduction from pm2.21 579. (Contributed by Mario Carneiro, 9-Feb-2017.) |
Ref | Expression |
---|---|
pm2.21dd.1 | ⊢ (𝜑 → 𝜓) |
pm2.21dd.2 | ⊢ (𝜑 → ¬ 𝜓) |
Ref | Expression |
---|---|
pm2.21dd | ⊢ (𝜑 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21dd.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | pm2.21dd.2 | . . 3 ⊢ (𝜑 → ¬ 𝜓) | |
3 | 2 | pm2.21d 581 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
4 | 1, 3 | mpd 13 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-in2 577 |
This theorem is referenced by: pm2.21fal 1304 pm2.21ddne 2328 ordtriexmidlem 4263 ordtri2or2exmidlem 4269 onsucelsucexmidlem 4272 wetriext 4319 reg3exmidlemwe 4321 nnm00 6125 phpm 6351 fidifsnen 6355 en2eqpr 6380 aptiprleml 6829 aptiprlemu 6830 uzdisj 9110 nn0disj 9148 addmodlteq 9400 frec2uzlt2d 9406 divalglemeunn 10321 divalglemeuneg 10323 zsupcllemex 10342 |
Copyright terms: Public domain | W3C validator |