Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > prarloclemup | Unicode version |
Description: Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 6693. (Contributed by Jim Kingdon, 10-Nov-2019.) |
Ref | Expression |
---|---|
prarloclemup | +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpllr 500 | . . 3 +Q0 ~Q0 ·Q0 | |
2 | simprl 497 | . . 3 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 | |
3 | simplr 496 | . . 3 +Q0 ~Q0 ·Q0 | |
4 | rspe 2412 | . . 3 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 | |
5 | 1, 2, 3, 4 | syl12anc 1167 | . 2 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 |
6 | 5 | exp31 356 | 1 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 102 w3a 919 wcel 1433 wrex 2349 cop 3401 csuc 4120 com 4331 (class class class)co 5532 c1o 6017 c2o 6018 coa 6021 cec 6127 ceq 6469 cnq 6470 cplq 6472 cmq 6473 ~Q0 ceq0 6476 +Q0 cplq0 6479 ·Q0 cmq0 6480 cnp 6481 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-4 1440 |
This theorem depends on definitions: df-bi 115 df-rex 2354 |
This theorem is referenced by: prarloclem3step 6686 |
Copyright terms: Public domain | W3C validator |