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 7311. (Contributed by Jim Kingdon, 10-Nov-2019.) |
Ref | Expression |
---|---|
prarloclemup | +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpllr 523 | . . 3 +Q0 ~Q0 ·Q0 | |
2 | simprl 520 | . . 3 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 | |
3 | simplr 519 | . . 3 +Q0 ~Q0 ·Q0 | |
4 | rspe 2481 | . . 3 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 | |
5 | 1, 2, 3, 4 | syl12anc 1214 | . 2 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 |
6 | 5 | exp31 361 | 1 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 962 wcel 1480 wrex 2417 cop 3530 csuc 4287 com 4504 (class class class)co 5774 c1o 6306 c2o 6307 coa 6310 cec 6427 ceq 7087 cnq 7088 cplq 7090 cmq 7091 ~Q0 ceq0 7094 +Q0 cplq0 7097 ·Q0 cmq0 7098 cnp 7099 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 |
This theorem depends on definitions: df-bi 116 df-rex 2422 |
This theorem is referenced by: prarloclem3step 7304 |
Copyright terms: Public domain | W3C validator |