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 1013 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 973 |
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 975 |
This theorem is referenced by: simpl1r 1044 simpr1r 1050 simp11r 1104 simp21r 1110 simp31r 1116 vtoclgft 2780 en2lp 4538 funprg 5248 nnsucsssuc 6471 ecopovtrn 6610 ecopovtrng 6613 addassnqg 7344 distrnqg 7349 ltsonq 7360 ltanqg 7362 ltmnqg 7363 distrnq0 7421 addassnq0 7424 prarloclem5 7462 recexprlem1ssl 7595 recexprlem1ssu 7596 mulasssrg 7720 distrsrg 7721 lttrsr 7724 ltsosr 7726 ltasrg 7732 mulextsr1lem 7742 mulextsr1 7743 axmulass 7835 axdistr 7836 dmdcanap 8639 lt2msq1 8801 lediv2 8807 xaddass2 9827 xlt2add 9837 modqdi 10348 expaddzaplem 10519 expaddzap 10520 expmulzap 10522 bdtrilem 11202 xrbdtri 11239 prmexpb 12105 mgmsscl 12615 cnptoprest 13033 ssblps 13219 ssbl 13220 rplogbchbase 13662 rplogbreexp 13665 relogbcxpbap 13677 lgssq 13735 |
Copyright terms: Public domain | W3C validator |