![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp3l | Unicode version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp3l |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 108 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant3 987 |
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 947 |
This theorem is referenced by: simpl3l 1019 simpr3l 1025 simp13l 1079 simp23l 1085 simp33l 1091 issod 4201 tfisi 4461 tfrlem5 6165 tfrlemibxssdm 6178 tfr1onlembxssdm 6194 tfrcllembxssdm 6207 ecopovtrn 6480 ecopovtrng 6483 addassnqg 7138 ltsonq 7154 ltanqg 7156 ltmnqg 7157 addassnq0 7218 mulasssrg 7501 distrsrg 7502 lttrsr 7505 ltsosr 7507 ltasrg 7513 mulextsr1lem 7522 mulextsr1 7523 axmulass 7608 axdistr 7609 lemul1 8273 reapmul1lem 8274 reapmul1 8275 mulcanap 8339 mulcanap2 8340 divassap 8363 divdirap 8370 div11ap 8373 muldivdirap 8380 divcanap5 8387 apmul1 8461 apmul2 8462 ltdiv1 8536 ltmuldiv 8542 ledivmul 8545 lemuldiv 8549 ltdiv2 8555 lediv2 8559 ltdiv23 8560 lediv23 8561 xaddass2 9546 xlt2add 9556 modqdi 10058 expaddzap 10230 expmulzap 10232 leisorel 10473 resqrtcl 10693 xrbdtri 10937 dvdscmulr 11370 dvdsmulcr 11371 dvdsadd2b 11388 dvdsgcd 11546 rpexp12i 11679 psmetlecl 12323 xmetlecl 12356 |
Copyright terms: Public domain | W3C validator |