![]() |
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 107 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant2 965 |
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 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 926 |
This theorem is referenced by: simpl2l 996 simpr2l 1002 simp12l 1056 simp22l 1062 simp32l 1068 issod 4146 funprg 5064 fsnunf 5497 f1oiso2 5606 ecopovtrn 6389 ecopovtrng 6392 addassnqg 6941 ltsonq 6957 ltanqg 6959 ltmnqg 6960 addassnq0 7021 recexprlem1ssu 7193 mulasssrg 7304 distrsrg 7305 lttrsr 7308 ltsosr 7310 ltasrg 7316 mulextsr1lem 7325 mulextsr1 7326 axmulass 7408 axdistr 7409 dmdcanap 8189 ltdiv2 8348 lediv2 8352 ltdiv23 8353 lediv23 8354 expaddzaplem 9998 expaddzap 9999 expmulzap 10001 expdivap 10006 leisorel 10242 fsumsplitsnun 10813 prmexpb 11408 |
Copyright terms: Public domain | W3C validator |