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 109 | . 2 | |
2 | 1 | 3ad2ant1 1002 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: simpl1r 1033 simpr1r 1039 simp11r 1093 simp21r 1099 simp31r 1105 vtoclgft 2731 en2lp 4464 funprg 5168 nnsucsssuc 6381 ecopovtrn 6519 ecopovtrng 6522 addassnqg 7183 distrnqg 7188 ltsonq 7199 ltanqg 7201 ltmnqg 7202 distrnq0 7260 addassnq0 7263 prarloclem5 7301 recexprlem1ssl 7434 recexprlem1ssu 7435 mulasssrg 7559 distrsrg 7560 lttrsr 7563 ltsosr 7565 ltasrg 7571 mulextsr1lem 7581 mulextsr1 7582 axmulass 7674 axdistr 7675 dmdcanap 8475 lt2msq1 8636 lediv2 8642 xaddass2 9646 xlt2add 9656 modqdi 10158 expaddzaplem 10329 expaddzap 10330 expmulzap 10332 bdtrilem 11003 xrbdtri 11038 prmexpb 11818 cnptoprest 12397 ssblps 12583 ssbl 12584 |
Copyright terms: Public domain | W3C validator |