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 6601. (Contributed by Jim Kingdon, 10-Nov-2019.) |
Ref | Expression |
---|---|
prarloclemup | +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpllr 486 | . . 3 +Q0 ~Q0 ·Q0 | |
2 | simprl 483 | . . 3 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 | |
3 | simplr 482 | . . 3 +Q0 ~Q0 ·Q0 | |
4 | rspe 2370 | . . 3 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 | |
5 | 1, 2, 3, 4 | syl12anc 1133 | . 2 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 |
6 | 5 | exp31 346 | 1 +Q0 ~Q0 ·Q0 +Q0 ~Q0 ·Q0 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 w3a 885 wcel 1393 wrex 2307 cop 3378 csuc 4102 com 4313 (class class class)co 5512 c1o 5994 c2o 5995 coa 5998 cec 6104 ceq 6377 cnq 6378 cplq 6380 cmq 6381 ~Q0 ceq0 6384 +Q0 cplq0 6387 ·Q0 cmq0 6388 cnp 6389 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 |
This theorem depends on definitions: df-bi 110 df-rex 2312 |
This theorem is referenced by: prarloclem3step 6594 |
Copyright terms: Public domain | W3C validator |