| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > simp1r | Unicode version | ||
| Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
| Ref | Expression |
|---|---|
| simp1r |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpr 110 |
. 2
| |
| 2 | 1 | 3ad2ant1 1021 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
| This theorem depends on definitions: df-bi 117 df-3an 983 |
| This theorem is referenced by: simpl1r 1052 simpr1r 1058 simp11r 1112 simp21r 1118 simp31r 1124 vtoclgft 2823 en2lp 4602 funprg 5324 nnsucsssuc 6578 ecopovtrn 6719 ecopovtrng 6722 addassnqg 7495 distrnqg 7500 ltsonq 7511 ltanqg 7513 ltmnqg 7514 distrnq0 7572 addassnq0 7575 prarloclem5 7613 recexprlem1ssl 7746 recexprlem1ssu 7747 mulasssrg 7871 distrsrg 7872 lttrsr 7875 ltsosr 7877 ltasrg 7883 mulextsr1lem 7893 mulextsr1 7894 axmulass 7986 axdistr 7987 dmdcanap 8795 lt2msq1 8958 lediv2 8964 xaddass2 9992 xlt2add 10002 modqdi 10537 expaddzaplem 10727 expaddzap 10728 expmulzap 10730 swrdspsleq 11120 bdtrilem 11550 xrbdtri 11587 bitsfzo 12266 prmexpb 12473 4sqlem18 12731 mgmsscl 13193 subgabl 13668 cnptoprest 14711 ssblps 14897 ssbl 14898 rplogbchbase 15422 rplogbreexp 15425 relogbcxpbap 15437 lgssq 15517 |
| Copyright terms: Public domain | W3C validator |