| 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 109 |
. 2
| |
| 2 | 1 | 3ad2ant3 1022 |
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 982 |
| This theorem is referenced by: simpl3l 1054 simpr3l 1060 simp13l 1114 simp23l 1120 simp33l 1126 issod 4365 tfisi 4634 tfrlem5 6399 tfrlemibxssdm 6412 tfr1onlembxssdm 6428 tfrcllembxssdm 6441 ecopovtrn 6718 ecopovtrng 6721 dftap2 7362 addassnqg 7494 ltsonq 7510 ltanqg 7512 ltmnqg 7513 addassnq0 7574 mulasssrg 7870 distrsrg 7871 lttrsr 7874 ltsosr 7876 ltasrg 7882 mulextsr1lem 7892 mulextsr1 7893 axmulass 7985 axdistr 7986 lemul1 8665 reapmul1lem 8666 reapmul1 8667 mulcanap 8737 mulcanap2 8738 divassap 8762 divdirap 8769 div11ap 8772 muldivdirap 8779 divcanap5 8786 apmul1 8860 apmul2 8861 ltdiv1 8940 ltmuldiv 8946 ledivmul 8949 lemuldiv 8953 ltdiv2 8959 lediv2 8963 ltdiv23 8964 lediv23 8965 xaddass2 9991 xlt2add 10001 modqdi 10535 expaddzap 10726 expmulzap 10728 leisorel 10980 resqrtcl 11282 xrbdtri 11529 dvdscmulr 12073 dvdsmulcr 12074 dvdsadd2b 12093 dvdsgcd 12275 rpexp12i 12419 pythagtriplem3 12532 pcpremul 12558 pceu 12560 pcqmul 12568 pcqdiv 12572 f1ocpbllem 13084 ercpbl 13105 erlecpbl 13106 cmn4 13583 ablsub4 13591 abladdsub4 13592 lidlsubcl 14191 psmetlecl 14748 xmetlecl 14781 |
| Copyright terms: Public domain | W3C validator |