![]() |
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 1018 |
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 980 |
This theorem is referenced by: simpl1r 1049 simpr1r 1055 simp11r 1109 simp21r 1115 simp31r 1121 vtoclgft 2787 en2lp 4553 funprg 5266 nnsucsssuc 6492 ecopovtrn 6631 ecopovtrng 6634 addassnqg 7380 distrnqg 7385 ltsonq 7396 ltanqg 7398 ltmnqg 7399 distrnq0 7457 addassnq0 7460 prarloclem5 7498 recexprlem1ssl 7631 recexprlem1ssu 7632 mulasssrg 7756 distrsrg 7757 lttrsr 7760 ltsosr 7762 ltasrg 7768 mulextsr1lem 7778 mulextsr1 7779 axmulass 7871 axdistr 7872 dmdcanap 8677 lt2msq1 8840 lediv2 8846 xaddass2 9868 xlt2add 9878 modqdi 10389 expaddzaplem 10560 expaddzap 10561 expmulzap 10563 bdtrilem 11242 xrbdtri 11279 prmexpb 12145 mgmsscl 12734 cnptoprest 13632 ssblps 13818 ssbl 13819 rplogbchbase 14261 rplogbreexp 14264 relogbcxpbap 14276 lgssq 14334 |
Copyright terms: Public domain | W3C validator |