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 508 | . 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 518 fimax2gtri 6763 finexdc 6764 difinfsn 6953 exmidfodomrlemr 7026 exmidfodomrlemrALT 7027 suplocexprlemru 7495 suplocsrlemb 7582 suplocsrlem 7584 supinfneg 9358 infsupneg 9359 xaddf 9595 xaddval 9596 hashunlem 10518 xrmaxiflemcl 10982 xrmaxiflemlub 10985 xrmaxltsup 10995 sumeq2 11096 fsumconst 11191 cncnp 12326 neitx 12364 dedekindeulemlu 12695 suplociccreex 12698 dedekindicclemlu 12704 cnplimclemr 12734 limccnp2cntop 12742 |
Copyright terms: Public domain | W3C validator |