Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simp1r | Unicode version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp1r |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 103 | . 2 | |
2 | 1 | 3ad2ant1 925 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 w3a 885 |
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 887 |
This theorem is referenced by: simpl1r 956 simpr1r 962 simp11r 1016 simp21r 1022 simp31r 1028 vtoclgft 2604 en2lp 4278 funprg 4949 nnsucsssuc 6071 ecopovtrn 6203 ecopovtrng 6206 addassnqg 6480 distrnqg 6485 ltsonq 6496 ltanqg 6498 ltmnqg 6499 distrnq0 6557 addassnq0 6560 prarloclem5 6598 recexprlem1ssl 6731 recexprlem1ssu 6732 mulasssrg 6843 distrsrg 6844 lttrsr 6847 ltsosr 6849 ltasrg 6855 mulextsr1lem 6864 mulextsr1 6865 axmulass 6947 axdistr 6948 dmdcanap 7698 lt2msq1 7851 lediv2 7857 expaddzaplem 9298 expaddzap 9299 expmulzap 9301 |
Copyright terms: Public domain | W3C validator |