![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp2r | Unicode version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp2r |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 109 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant2 986 |
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: simpl2r 1018 simpr2r 1024 simp12r 1078 simp22r 1084 simp32r 1090 issod 4201 funprg 5131 fsnunf 5574 f1oiso2 5682 tfrlemibxssdm 6178 ecopovtrn 6480 ecopovtrng 6483 addassnqg 7138 ltsonq 7154 ltanqg 7156 ltmnqg 7157 addassnq0 7218 recexprlem1ssl 7389 mulasssrg 7501 distrsrg 7502 lttrsr 7505 ltsosr 7507 ltasrg 7513 mulextsr1lem 7522 mulextsr1 7523 axmulass 7608 axdistr 7609 dmdcanap 8395 lediv2 8559 ltdiv23 8560 lediv23 8561 xaddass2 9546 xlt2add 9556 expaddzaplem 10229 expaddzap 10230 expmulzap 10232 expdivap 10237 leisorel 10473 bdtrilem 10902 xrbdtri 10937 fldivndvdslt 11480 prmexpb 11675 cnptoprest 12250 ssblps 12414 ssbl 12415 tgqioo 12533 |
Copyright terms: Public domain | W3C validator |