![]() |
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 4337 tfisi 4604 tfrlem5 6340 tfrlemibxssdm 6353 tfr1onlembxssdm 6369 tfrcllembxssdm 6382 ecopovtrn 6659 ecopovtrng 6662 dftap2 7281 addassnqg 7412 ltsonq 7428 ltanqg 7430 ltmnqg 7431 addassnq0 7492 mulasssrg 7788 distrsrg 7789 lttrsr 7792 ltsosr 7794 ltasrg 7800 mulextsr1lem 7810 mulextsr1 7811 axmulass 7903 axdistr 7904 lemul1 8581 reapmul1lem 8582 reapmul1 8583 mulcanap 8653 mulcanap2 8654 divassap 8678 divdirap 8685 div11ap 8688 muldivdirap 8695 divcanap5 8702 apmul1 8776 apmul2 8777 ltdiv1 8856 ltmuldiv 8862 ledivmul 8865 lemuldiv 8869 ltdiv2 8875 lediv2 8879 ltdiv23 8880 lediv23 8881 xaddass2 9902 xlt2add 9912 modqdi 10425 expaddzap 10598 expmulzap 10600 leisorel 10852 resqrtcl 11073 xrbdtri 11319 dvdscmulr 11862 dvdsmulcr 11863 dvdsadd2b 11882 dvdsgcd 12048 rpexp12i 12190 pythagtriplem3 12302 pcpremul 12328 pceu 12330 pcqmul 12338 pcqdiv 12342 f1ocpbllem 12790 ercpbl 12810 erlecpbl 12811 cmn4 13261 ablsub4 13269 abladdsub4 13270 lidlsubcl 13820 psmetlecl 14311 xmetlecl 14344 |
Copyright terms: Public domain | W3C validator |