![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp1l | Unicode version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp1l |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 109 |
. 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: simpl1l 1050 simpr1l 1056 simp11l 1110 simp21l 1116 simp31l 1122 en2lp 4571 tfisi 4604 funprg 5285 nnsucsssuc 6516 ecopovtrn 6657 ecopovtrng 6660 addassnqg 7410 distrnqg 7415 ltsonq 7426 ltanqg 7428 ltmnqg 7429 distrnq0 7487 addassnq0 7490 mulasssrg 7786 distrsrg 7787 lttrsr 7790 ltsosr 7792 ltasrg 7798 mulextsr1lem 7808 mulextsr1 7809 axmulass 7901 axdistr 7902 dmdcanap 8708 lt2msq1 8871 ltdiv2 8873 lediv2 8877 xaddass 9898 xaddass2 9899 xlt2add 9909 modqdi 10422 expaddzaplem 10593 expaddzap 10594 expmulzap 10596 resqrtcl 11069 bdtrilem 11278 bdtri 11279 xrbdtri 11315 prmexpb 12182 4sqlem18 12439 subgabl 13266 opprringbg 13427 cnptoprest 14191 ssblps 14377 ssbl 14378 rplogbchbase 14820 rplogbreexp 14823 relogbcxpbap 14835 lgssq 14894 |
Copyright terms: Public domain | W3C validator |