Metamath Proof Explorer
Description: Value of the less-than-or-equal-to relation is unchanged.
(Contributed by Zhi Wang, 20-Sep-2024) (Proof shortened by AV, 12-Nov-2024)
|
|
Ref |
Expression |
|
Hypotheses |
prstcnid.c |
No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |- |
|
|
prstcnid.k |
|
|
|
prstcle.l |
|
|
Assertion |
prstcleval |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
prstcnid.c |
Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |- |
2 |
|
prstcnid.k |
|
3 |
|
prstcle.l |
|
4 |
|
pleid |
|
5 |
|
slotsdifplendx2 |
|
6 |
5
|
simpli |
|
7 |
5
|
simpri |
|
8 |
1 2 4 6 7
|
prstcnid |
|
9 |
3 8
|
eqtrd |
|