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 607. (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 609 | . 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 605 |
This theorem is referenced by: pm2.21fal 1362 pm2.21ddne 2417 ordtriexmidlem 4490 ordtri2or2exmidlem 4497 onsucelsucexmidlem 4500 wetriext 4548 reg3exmidlemwe 4550 nntr2 6462 nnm00 6488 phpm 6822 fidifsnen 6827 dif1enen 6837 infnfi 6852 en2eqpr 6864 aptiprleml 7571 aptiprlemu 7572 uzdisj 10018 nn0disj 10063 addmodlteq 10323 frec2uzlt2d 10329 iseqf1olemab 10414 iseqf1olemmo 10417 hashennnuni 10681 hashfiv01gt1 10684 xrmaxiflemab 11174 xrmaxiflemlub 11175 xrmaxltsup 11185 xrbdtri 11203 divalglemeunn 11843 divalglemeuneg 11845 zsupcllemex 11864 ennnfonelemk 12270 cnplimclemle 13178 efltlemlt 13236 trilpolemlt1 13754 neapmkvlem 13779 |
Copyright terms: Public domain | W3C validator |