![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp-4r | Unicode version |
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Ref | Expression |
---|---|
simp-4r |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpllr 534 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantr 276 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: simp-5r 544 fimax2gtri 6915 finexdc 6916 dcfi 6994 difinfsn 7113 nnnninfeq2 7141 nninfisol 7145 exmidfodomrlemr 7215 exmidfodomrlemrALT 7216 suplocexprlemru 7732 suplocsrlemb 7819 suplocsrlem 7821 aptap 8621 supinfneg 9609 infsupneg 9610 xaddf 9858 xaddval 9859 nn0ltexp2 10703 hashunlem 10798 xrmaxiflemcl 11267 xrmaxiflemlub 11270 xrmaxltsup 11280 sumeq2 11381 fsumconst 11476 prodeq2 11579 fprodconst 11642 sgrpidmndm 12843 mhmmnd 13011 ghmcmn 13163 issrg 13217 cncnp 14026 neitx 14064 dedekindeulemlu 14395 suplociccreex 14398 dedekindicclemlu 14404 cnplimclemr 14434 limccnp2cntop 14442 logbgcd1irrap 14684 lgsval 14701 |
Copyright terms: Public domain | W3C validator |