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 4501 ordtri2or2exmidlem 4508 onsucelsucexmidlem 4511 wetriext 4559 reg3exmidlemwe 4561 nntr2 6479 nnm00 6505 phpm 6839 fidifsnen 6844 dif1enen 6854 infnfi 6869 en2eqpr 6881 aptiprleml 7588 aptiprlemu 7589 uzdisj 10036 nn0disj 10081 addmodlteq 10341 frec2uzlt2d 10347 iseqf1olemab 10432 iseqf1olemmo 10435 hashennnuni 10700 hashfiv01gt1 10703 xrmaxiflemab 11197 xrmaxiflemlub 11198 xrmaxltsup 11208 xrbdtri 11226 divalglemeunn 11867 divalglemeuneg 11869 zsupcllemex 11888 ennnfonelemk 12342 cnplimclemle 13390 efltlemlt 13448 trilpolemlt1 14033 neapmkvlem 14058 |
Copyright terms: Public domain | W3C validator |