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 612. (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 614 | . 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 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 |