![]() |
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 110 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant2 1019 |
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 980 |
This theorem is referenced by: simpl2r 1051 simpr2r 1057 simp12r 1111 simp22r 1117 simp32r 1123 issod 4321 funprg 5268 fsnunf 5719 f1oiso2 5831 tfrlemibxssdm 6331 ecopovtrn 6635 ecopovtrng 6638 dftap2 7253 addassnqg 7384 ltsonq 7400 ltanqg 7402 ltmnqg 7403 addassnq0 7464 recexprlem1ssl 7635 mulasssrg 7760 distrsrg 7761 lttrsr 7764 ltsosr 7766 ltasrg 7772 mulextsr1lem 7782 mulextsr1 7783 axmulass 7875 axdistr 7876 dmdcanap 8682 lediv2 8851 ltdiv23 8852 lediv23 8853 xaddass2 9873 xlt2add 9883 expaddzaplem 10566 expaddzap 10567 expmulzap 10569 expdivap 10574 leisorel 10820 bdtrilem 11250 xrbdtri 11287 fldivndvdslt 11943 prmexpb 12154 pcpremul 12296 pcdiv 12305 pcqmul 12306 pcqdiv 12310 f1ocpbllem 12737 ercpbl 12756 erlecpbl 12757 cmn4 13114 ablsub4 13122 abladdsub4 13123 cnptoprest 13879 ssblps 14065 ssbl 14066 tgqioo 14187 rplogbchbase 14508 |
Copyright terms: Public domain | W3C validator |