![]() |
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 107 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3ad2ant1 964 |
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 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 926 |
This theorem is referenced by: simpl1l 994 simpr1l 1000 simp11l 1054 simp21l 1060 simp31l 1066 en2lp 4370 tfisi 4402 funprg 5064 nnsucsssuc 6253 ecopovtrn 6387 ecopovtrng 6390 addassnqg 6939 distrnqg 6944 ltsonq 6955 ltanqg 6957 ltmnqg 6958 distrnq0 7016 addassnq0 7019 mulasssrg 7302 distrsrg 7303 lttrsr 7306 ltsosr 7308 ltasrg 7314 mulextsr1lem 7323 mulextsr1 7324 axmulass 7406 axdistr 7407 dmdcanap 8187 lt2msq1 8344 ltdiv2 8346 lediv2 8350 modqdi 9795 expaddzaplem 9994 expaddzap 9995 expmulzap 9997 resqrtcl 10458 prmexpb 11404 |
Copyright terms: Public domain | W3C validator |