| 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 1020 |
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 982 |
| This theorem is referenced by: simpl1r 1051 simpr1r 1057 simp11r 1111 simp21r 1117 simp31r 1123 vtoclgft 2822 en2lp 4601 funprg 5323 nnsucsssuc 6577 ecopovtrn 6718 ecopovtrng 6721 addassnqg 7494 distrnqg 7499 ltsonq 7510 ltanqg 7512 ltmnqg 7513 distrnq0 7571 addassnq0 7574 prarloclem5 7612 recexprlem1ssl 7745 recexprlem1ssu 7746 mulasssrg 7870 distrsrg 7871 lttrsr 7874 ltsosr 7876 ltasrg 7882 mulextsr1lem 7892 mulextsr1 7893 axmulass 7985 axdistr 7986 dmdcanap 8794 lt2msq1 8957 lediv2 8963 xaddass2 9991 xlt2add 10001 modqdi 10535 expaddzaplem 10725 expaddzap 10726 expmulzap 10728 bdtrilem 11521 xrbdtri 11558 bitsfzo 12237 prmexpb 12444 4sqlem18 12702 mgmsscl 13164 subgabl 13639 cnptoprest 14682 ssblps 14868 ssbl 14869 rplogbchbase 15393 rplogbreexp 15396 relogbcxpbap 15408 lgssq 15488 |
| Copyright terms: Public domain | W3C validator |