![]() |
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 103 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant3 926 |
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 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 886 |
This theorem is referenced by: simpl3r 959 simpr3r 965 simp13r 1019 simp23r 1025 simp33r 1031 issod 4047 tfisi 4253 fvun1 5182 f1oiso2 5409 tfrlem5 5871 ecopovtrn 6139 ecopovtrng 6142 addassnqg 6366 ltsonq 6382 ltanqg 6384 ltmnqg 6385 addassnq0 6445 mulasssrg 6686 distrsrg 6687 lttrsr 6690 ltsosr 6692 ltasrg 6698 mulextsr1lem 6706 mulextsr1 6707 axmulass 6757 axdistr 6758 reapmul1 7379 mulcanap 7428 mulcanap2 7429 divassap 7451 divdirap 7456 div11ap 7459 apmul1 7546 ltdiv1 7615 ltmuldiv 7621 ledivmul 7624 lemuldiv 7628 lediv2 7638 ltdiv23 7639 lediv23 7640 expaddzap 8953 expmulzap 8955 |
Copyright terms: Public domain | W3C validator |