![]() |
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 607 |
. 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 605 |
This theorem is referenced by: pm2.24d 612 pm2.53 712 pm2.82 802 pm4.81dc 894 dedlema 954 alexim 1625 eqneqall 2319 elnelall 2416 sotritric 4254 ltxrlt 7854 zltnle 9124 elfzonlteqm1 10018 qltnle 10054 hashfzp1 10602 dfgcd2 11738 bj-fast 13123 |
Copyright terms: Public domain | W3C validator |