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 523 | . 2 | |
2 | 1 | adantr 274 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
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 is referenced by: simp-5r 533 fimax2gtri 6788 finexdc 6789 difinfsn 6978 exmidfodomrlemr 7051 exmidfodomrlemrALT 7052 suplocexprlemru 7520 suplocsrlemb 7607 suplocsrlem 7609 supinfneg 9383 infsupneg 9384 xaddf 9620 xaddval 9621 hashunlem 10543 xrmaxiflemcl 11007 xrmaxiflemlub 11010 xrmaxltsup 11020 sumeq2 11121 fsumconst 11216 prodeq2 11319 cncnp 12388 neitx 12426 dedekindeulemlu 12757 suplociccreex 12760 dedekindicclemlu 12766 cnplimclemr 12796 limccnp2cntop 12804 |
Copyright terms: Public domain | W3C validator |