![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp1l | Unicode version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp1l |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 108 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant1 967 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 929 |
This theorem is referenced by: simpl1l 997 simpr1l 1003 simp11l 1057 simp21l 1063 simp31l 1069 en2lp 4398 tfisi 4430 funprg 5098 nnsucsssuc 6293 ecopovtrn 6429 ecopovtrng 6432 addassnqg 7038 distrnqg 7043 ltsonq 7054 ltanqg 7056 ltmnqg 7057 distrnq0 7115 addassnq0 7118 mulasssrg 7401 distrsrg 7402 lttrsr 7405 ltsosr 7407 ltasrg 7413 mulextsr1lem 7422 mulextsr1 7423 axmulass 7505 axdistr 7506 dmdcanap 8286 lt2msq1 8443 ltdiv2 8445 lediv2 8449 xaddass 9435 xaddass2 9436 xlt2add 9446 modqdi 9948 expaddzaplem 10129 expaddzap 10130 expmulzap 10132 resqrtcl 10593 bdtrilem 10801 bdtri 10802 xrbdtri 10835 prmexpb 11572 cnptoprest 12105 ssblps 12226 ssbl 12227 |
Copyright terms: Public domain | W3C validator |