![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp3r | Unicode version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp3r |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 110 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant3 1020 |
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: simpl3r 1053 simpr3r 1059 simp13r 1113 simp23r 1119 simp33r 1125 issod 4319 tfisi 4586 fvun1 5582 f1oiso2 5827 tfrlem5 6314 tfr1onlembxssdm 6343 tfrcllembxssdm 6356 ecopovtrn 6631 ecopovtrng 6634 dftap2 7249 addassnqg 7380 ltsonq 7396 ltanqg 7398 ltmnqg 7399 addassnq0 7460 mulasssrg 7756 distrsrg 7757 lttrsr 7760 ltsosr 7762 ltasrg 7768 mulextsr1lem 7778 mulextsr1 7779 axmulass 7871 axdistr 7872 reapmul1 8551 mulcanap 8621 mulcanap2 8622 divassap 8646 divdirap 8653 div11ap 8656 apmul1 8744 ltdiv1 8824 ltmuldiv 8830 ledivmul 8833 lemuldiv 8837 lediv2 8847 ltdiv23 8848 lediv23 8849 xaddass2 9869 xlt2add 9879 modqdi 10391 expaddzap 10563 expmulzap 10565 leisorel 10816 resqrtcl 11037 xrbdtri 11283 dvdsgcd 12012 rpexp12i 12154 pythagtriplem4 12267 pythagtriplem11 12273 pythagtriplem13 12275 pcpremul 12292 pceu 12294 pcqmul 12302 pcqdiv 12306 f1ocpbllem 12730 ercpbl 12749 erlecpbl 12750 cmn4 13106 ablsub4 13114 abladdsub4 13115 psmetlecl 13770 xmetlecl 13803 xblcntrps 13849 xblcntr 13850 |
Copyright terms: Public domain | W3C validator |