![]() |
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 617. (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 619 | . 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-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 |