![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > pm2.24 | Unicode version |
Description: Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
Ref | Expression |
---|---|
pm2.24 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.21 618 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | com12 30 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in2 616 |
This theorem is referenced by: pm2.24d 623 pm2.53 723 pm2.82 813 pm4.81dc 909 dedlema 971 alexim 1656 eqneqall 2370 elnelall 2467 sotritric 4342 ltxrlt 8052 zltnle 9328 elfzonlteqm1 10239 qltnle 10275 hashfzp1 10835 dfgcd2 12046 oddprmdvds 12385 bj-fast 14946 nnnotnotr 15195 |
Copyright terms: Public domain | W3C validator |