![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.21dd | Unicode version |
Description: A contradiction implies anything. Deduction from pm2.21 589. (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 591 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpd 13 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-in2 587 |
This theorem is referenced by: pm2.21fal 1334 pm2.21ddne 2365 ordtriexmidlem 4395 ordtri2or2exmidlem 4401 onsucelsucexmidlem 4404 wetriext 4451 reg3exmidlemwe 4453 nntr2 6353 nnm00 6379 phpm 6712 fidifsnen 6717 dif1enen 6727 infnfi 6742 en2eqpr 6754 aptiprleml 7395 aptiprlemu 7396 uzdisj 9766 nn0disj 9808 addmodlteq 10064 frec2uzlt2d 10070 iseqf1olemab 10155 iseqf1olemmo 10158 hashennnuni 10418 hashfiv01gt1 10421 xrmaxiflemab 10908 xrmaxiflemlub 10909 xrmaxltsup 10919 xrbdtri 10937 divalglemeunn 11466 divalglemeuneg 11468 zsupcllemex 11487 ennnfonelemk 11758 cnplimclemle 12593 trilpolemlt1 12926 |
Copyright terms: Public domain | W3C validator |