![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp2l | Unicode version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp2l |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 108 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant2 966 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 927 |
This theorem is referenced by: simpl2l 997 simpr2l 1003 simp12l 1057 simp22l 1063 simp32l 1069 issod 4157 funprg 5079 fsnunf 5513 f1oiso2 5622 ecopovtrn 6405 ecopovtrng 6408 addassnqg 7004 ltsonq 7020 ltanqg 7022 ltmnqg 7023 addassnq0 7084 recexprlem1ssu 7256 mulasssrg 7367 distrsrg 7368 lttrsr 7371 ltsosr 7373 ltasrg 7379 mulextsr1lem 7388 mulextsr1 7389 axmulass 7471 axdistr 7472 dmdcanap 8252 ltdiv2 8411 lediv2 8415 ltdiv23 8416 lediv23 8417 expaddzaplem 10061 expaddzap 10062 expmulzap 10064 expdivap 10069 leisorel 10305 fsumsplitsnun 10876 prmexpb 11471 |
Copyright terms: Public domain | W3C validator |