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 7304. (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 2479 | . . 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 2415 cop 3525 csuc 4282 com 4499 (class class class)co 5767 c1o 6299 c2o 6300 coa 6303 cec 6420 ceq 7080 cnq 7081 cplq 7083 cmq 7084 ~Q0 ceq0 7087 +Q0 cplq0 7090 ·Q0 cmq0 7091 cnp 7092 |
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 2420 |
This theorem is referenced by: prarloclem3step 7297 |
Copyright terms: Public domain | W3C validator |