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 1003 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 963 |
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 965 |
This theorem is referenced by: simpl1r 1034 simpr1r 1040 simp11r 1094 simp21r 1100 simp31r 1106 vtoclgft 2762 en2lp 4513 funprg 5220 nnsucsssuc 6439 ecopovtrn 6577 ecopovtrng 6580 addassnqg 7302 distrnqg 7307 ltsonq 7318 ltanqg 7320 ltmnqg 7321 distrnq0 7379 addassnq0 7382 prarloclem5 7420 recexprlem1ssl 7553 recexprlem1ssu 7554 mulasssrg 7678 distrsrg 7679 lttrsr 7682 ltsosr 7684 ltasrg 7690 mulextsr1lem 7700 mulextsr1 7701 axmulass 7793 axdistr 7794 dmdcanap 8595 lt2msq1 8756 lediv2 8762 xaddass2 9774 xlt2add 9784 modqdi 10291 expaddzaplem 10462 expaddzap 10463 expmulzap 10465 bdtrilem 11138 xrbdtri 11173 prmexpb 12026 cnptoprest 12650 ssblps 12836 ssbl 12837 rplogbchbase 13278 rplogbreexp 13281 relogbcxpbap 13293 |
Copyright terms: Public domain | W3C validator |